# 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.

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

### Covering relation #

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.