mathlib3 documentation

data.nat.succ_pred

Successors and predecessors of naturals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 nat.succ_iterate (a n : ) :
nat.succ^[n] a = a + n
theorem nat.pred_iterate (a n : ) :
nat.pred^[n] a = a - n
@[protected, instance]
@[protected, instance]

Covering relation #

@[protected]
theorem nat.covby_iff_succ_eq {m n : } :
m n m + 1 = n
@[simp, norm_cast]
theorem fin.coe_covby_iff {n : } {a b : fin n} :
a b a b
theorem covby.coe_fin {n : } {a b : fin n} :
a b a b

Alias of the reverse direction of fin.coe_covby_iff.