def Nat.cases {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) (n : ℕ) : α n

Equations

• (hzero :>ₙ hsucc) 0 = hzero
• (hzero :>ₙ hsucc) n.succ = hsucc n

def Nat.«term_:>ₙ_» : Lean.TrailingParserDescr

Equations

• Nat.«term_:>ₙ_» = Lean.ParserDescr.trailingNode `Nat.«term_:>ₙ_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :>ₙ ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem Nat.cases_zero {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) : (hzero :>ₙ hsucc) 0 = hzero

@[simp]

theorem Nat.cases_succ {α : ℕ → Sort u} (hzero : α 0) (hsucc : (n : ℕ) → α (n + 1)) (n : ℕ) : (hzero :>ₙ hsucc) (n + 1) = hsucc n

@[simp]

theorem Nat.ne_step_max (n m : ℕ) : n ≠ max n m + 1

@[simp]

theorem Nat.ne_step_max' (n m : ℕ) : n ≠ max m n + 1

theorem Nat.rec_eq {α : Sort u_1} (a : α) (f₁ f₂ : ℕ → α → α) (n : ℕ) (H : ∀ m < n, ∀ (a : α), f₁ m a = f₂ m a) : rec a f₁ n = rec a f₂ n

theorem Nat.least_number (P : ℕ → Prop) (hP : ∃ (x : ℕ), P x) : ∃ (x : ℕ), P x ∧ ∀ z < x, ¬P z

def Nat.toFin (n a✝ : ℕ) : Option (Fin n)

Equations

• n.toFin x = if hx : x < n then some ⟨x, hx⟩ else none

theorem Nat.zero_lt_of_not_zero {n : ℕ} (hn : n ≠ 0) : 0 < n

theorem Nat.one_le_of_bodd {n : ℕ} (h : n.bodd = true) : 1 ≤ n

theorem Nat.pair_le_pair_of_le {a₁ a₂ b₁ b₂ : ℕ} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : pair a₁ b₁ ≤ pair a₂ b₂