Successors and predecessors of integers

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

@[reducible, inline]

instance Int.instSuccOrder : SuccOrder ℤ

instance Int.instSuccAddOrder : SuccAddOrder ℤ

@[reducible, inline]

instance Int.instPredOrder : PredOrder ℤ

instance Int.instPredSubOrder : PredSubOrder ℤ

@[simp]

theorem Int.succ_eq_succ : Order.succ = succ

@[simp]

theorem Int.pred_eq_pred : Order.pred = pred

instance Int.instIsSuccArchimedean : IsSuccArchimedean ℤ

instance Int.instIsPredArchimedean : IsPredArchimedean ℤ

Covering relation

@[simp]

theorem Int.natCast_covBy {a b : ℕ} : ↑a ⋖ ↑b ↔ a ⋖ b

theorem CovBy.intCast {a b : ℕ} : a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of Int.natCast_covBy.