# Successors and predecessors of integers #

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

@[reducible, inline]
Equations
@[reducible, inline]
Equations
@[simp]
theorem Int.succ_eq_succ :
Order.succ = Int.succ
@[simp]
theorem Int.pred_eq_pred :
Order.pred = Int.pred
@[deprecated Order.one_le_iff_pos]
theorem Int.pos_iff_one_le {a : } :
0 < a 1 a
@[deprecated Order.succ_iterate]
theorem Int.succ_iterate (a : ) (n : ) :
= a + n
@[deprecated Order.pred_iterate]
theorem Int.pred_iterate (a : ) (n : ) :
= a - n
Equations
Equations

### Covering relation #

theorem Int.covBy_iff_succ_eq {m : } {n : } :
m n m + 1 = n
@[deprecated Order.sub_one_covBy]
theorem Int.sub_one_covBy (z : ) :
z - 1 z
theorem Int.covBy_add_one (z : ) :
z z + 1
@[simp]
theorem Int.natCast_covBy {a : } {b : } :
a b a b
theorem CovBy.intCast {a : } {b : } :
a ba b

Alias of the reverse direction of Int.natCast_covBy.

@[deprecated Int.natCast_covBy]
theorem Nat.cast_int_covBy_iff {a : } {b : } :
a b a b

Alias of Int.natCast_covBy.

@[deprecated CovBy.intCast]
theorem CovBy.cast_int {a : } {b : } :
a ba b

Alias of the reverse direction of Int.natCast_covBy.

Alias of the reverse direction of Int.natCast_covBy.