# Successors and predecessors of naturals #

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

source
@[reducible, inline]
instance Nat.instSuccOrder :
SuccOrder ℕ
Equations

- Nat.instSuccOrder = SuccOrder.ofSuccLeIff Nat.succ ⋯

source
instance Nat.instSuccAddOrder :
SuccAddOrder ℕ
Equations

- Nat.instSuccAddOrder = { toSuccOrder := Nat.instSuccOrder, succ_eq_add_one := Nat.instSuccAddOrder._proof_1 }

source
@[reducible, inline]
instance Nat.instPredOrder :
PredOrder ℕ
Equations

- Nat.instPredOrder = { pred := Nat.pred, pred_le := Nat.pred_le, min_of_le_pred := @Nat.instPredOrder._proof_1, le_pred_of_lt := @Nat.instPredOrder._proof_2 }

source
instance Nat.instPredSubOrder :
PredSubOrder ℕ
Equations

- Nat.instPredSubOrder = { toPredOrder := Nat.instPredOrder, pred_eq_sub_one := Nat.instPredSubOrder._proof_1 }

source
@[simp]
theorem Nat.succ_eq_succ :
Order.succ = succ
source
@[simp]
theorem Nat.pred_eq_pred :
Order.pred = pred
source
theorem Nat.succ_iterate (a n : ℕ) :
succ^[n] a = a + n
source
theorem Nat.pred_iterate (a n : ℕ) :
pred^[n] a = a - n
source
theorem Nat.le_succ_iff_eq_or_le {m n : ℕ} :
m ≤ n.succ ↔ m = n.succ ∨ m ≤ n
source
instance Nat.instIsSuccArchimedean :
IsSuccArchimedean ℕ
source
instance Nat.instIsPredArchimedean :
IsPredArchimedean ℕ
source
theorem Nat.forall_ne_zero_iff (P : ℕ → Prop) :
(∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)
source
@[simp]
theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} :
↑a ⋖ ↑b ↔ a ⋖ b
source
theorem CovBy.coe_fin {n : ℕ} {a b : Fin n} :
a ⋖ b → ↑a ⋖ ↑b

Alias of the reverse direction of `Fin.coe_covBy_iff`.

source
@[simp]
theorem withBotSucc_zero :
WithBot.succ 0 = 1
source
@[simp]
theorem withBotSucc_one :
WithBot.succ 1 = 2