Successors and predecessors of naturals

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

@[implicit_reducible]

instance Nat.instSuccOrder : SuccOrder ℕ

@[implicit_reducible]

instance Nat.instSuccAddOrder : SuccAddOrder ℕ

@[implicit_reducible]

instance Nat.instPredOrder : PredOrder ℕ

@[implicit_reducible]

instance Nat.instPredSubOrder : PredSubOrder ℕ

@[simp]

theorem Nat.succ_eq_succ : Order.succ = succ

@[simp]

theorem Nat.pred_eq_pred : Order.pred = pred

theorem Nat.succ_iterate (a n : ℕ) : succ^[n] a = a + n

theorem Nat.pred_iterate (a n : ℕ) : pred^[n] a = a - n

@[simp]

theorem Nat.covBy_iff_add_one_eq {m n : ℕ} : m ⋖ n ↔ m + 1 = n

A special case of Order.covBy_iff_add_one_eq for use by simp.

theorem Nat.le_succ_iff_eq_or_le {m n : ℕ} : m ≤ n.succ ↔ m = n.succ ∨ m ≤ n

instance Nat.instIsSuccArchimedean : IsSuccArchimedean ℕ

instance Nat.instIsPredArchimedean : IsPredArchimedean ℕ

theorem Nat.forall_ne_zero_iff (P : ℕ → Prop) : (∀ (i : ℕ), i ≠ 0 → P i) ↔ ∀ (i : ℕ), P (i + 1)

@[simp]

theorem Fin.covBy_iff {n : ℕ} {a b : Fin n} : a ⋖ b ↔ ↑a ⋖ ↑b

@[deprecated Fin.covBy_iff "use Fin.covBy_iff.symm instead" (since := "2026-02-13")]

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 forward direction of Fin.covBy_iff.

@[simp]

theorem withBotSucc_zero : WithBot.succ 0 = 1

@[simp]

theorem withBotSucc_one : WithBot.succ 1 = 2