Documentation

Mathlib.Data.Nat.SuccPred

Successors and predecessors of naturals #

In this file, we show that is both an archimedean succOrder and an archimedean predOrder.

@[reducible, inline]
Equations
@[simp]
theorem Nat.succ_eq_succ :
Order.succ = Nat.succ
@[simp]
theorem Nat.pred_eq_pred :
Order.pred = Nat.pred
theorem Nat.succ_iterate (a : ) (n : ) :
Nat.succ^[n] a = a + n
theorem Nat.pred_iterate (a : ) (n : ) :
Nat.pred^[n] a = a - n
theorem Nat.le_succ_iff_eq_or_le {m : } {n : } :
m n.succ m = n.succ m n
theorem Nat.forall_ne_zero_iff (P : Prop) :
(∀ (i : ), i 0P i) ∀ (i : ), P (i + 1)

Covering relation #

@[deprecated Order.covBy_iff_add_one_eq]
theorem Nat.covBy_iff_succ_eq {m : } {n : } :
m n m + 1 = n
@[simp]
theorem Fin.coe_covBy_iff {n : } {a : Fin n} {b : Fin n} :
a b a b
theorem CovBy.coe_fin {n : } {a : Fin n} {b : Fin n} :
a ba b

Alias of the reverse direction of Fin.coe_covBy_iff.