mathlib documentation

data.int.succ_pred

Successors and predecessors of integers #

In this file, we show that is both an archimedean succ_order and an archimedean pred_order.

@[protected, instance, reducible]
Equations
@[protected, instance, reducible]
Equations
theorem int.pos_iff_one_le {a : } :
0 < a 1 a
theorem int.succ_iterate (a : ) (n : ) :
theorem int.pred_iterate (a : ) (n : ) :
@[protected, instance]
@[protected, instance]

Covering relation #

@[protected]
theorem int.covby_iff_succ_eq {m n : } :
m n m + 1 = n
@[simp, norm_cast]
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.