Successors and predecessors of integers

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

@[implicit_reducible]

instance Int.instSuccOrder : SuccOrder ℤ

Equations

• Int.instSuccOrder = { succ := Int.succ, le_succ := Int.instSuccOrder._proof_2, max_of_succ_le := @Int.instSuccOrder._proof_3, succ_le_of_lt := @Int.instSuccOrder._proof_4 }

@[implicit_reducible]

instance Int.instSuccAddOrder : SuccAddOrder ℤ

Equations

• Int.instSuccAddOrder = { toSuccOrder := Int.instSuccOrder, succ_eq_add_one := Int.instSuccAddOrder._proof_1 }

@[implicit_reducible]

instance Int.instPredOrder : PredOrder ℤ

Equations

• Int.instPredOrder = { pred := Int.pred, pred_le := Int.instPredOrder._proof_1, min_of_le_pred := @Int.instPredOrder._proof_2, le_pred_of_lt := ⋯ }

@[implicit_reducible]

instance Int.instPredSubOrder : PredSubOrder ℤ

Equations

• Int.instPredSubOrder = { toPredOrder := Int.instPredOrder, pred_eq_sub_one := Int.instPredSubOrder._proof_1 }

@[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.