Documentation

Mathlib.Data.Int.SuccPred

Successors and predecessors of integers #

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

@[reducible]
Equations
  • One or more equations did not get rendered due to their size.
@[reducible]
Equations
  • One or more equations did not get rendered due to their size.
@[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

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 ba b

Alias of the reverse direction of Nat.cast_int_covby_iff.