Successors and predecessors of integers

In this file, we show that ℤ is both an archimedean SuccOrder and an archimedean PredOrder.

@[reducible]

instance Int.instSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : SuccOrder ℤ

@[reducible]

instance Int.instPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : PredOrder ℤ

@[simp]

theorem Int.succ_eq_succ : Order.succ = Int.succ

@[simp]

theorem Int.pred_eq_pred : Order.pred = Int.pred

theorem Int.pos_iff_one_le {a : ℤ} : 0 < a ↔ 1 ≤ a

theorem Int.succ_iterate (a : ℤ) (n : ℕ) : Int.succ^[n] a = a + ↑n

theorem Int.pred_iterate (a : ℤ) (n : ℕ) : Int.pred^[n] a = a - ↑n

instance Int.instIsSuccArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingInstSuccOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : IsSuccArchimedean ℤ

instance Int.instIsPredArchimedeanIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingInstPredOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : IsPredArchimedean ℤ

Covering relation

theorem Int.covby_iff_succ_eq {m : ℤ} {n : ℤ} : m ⋖ n ↔ m + 1 = n

@[simp]

theorem Int.sub_one_covby (z : ℤ) : z - 1 ⋖ z

@[simp]

theorem Int.covby_add_one (z : ℤ) : z ⋖ z + 1

@[simp]

theorem Nat.cast_int_covby_iff {a : ℕ} {b : ℕ} : ↑a ⋖ ↑b ↔ a ⋖ b

theorem Covby.cast_int {a : ℕ} {b : ℕ} : a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Nat.cast_int_covby_iff.