instance Nat.preorder : Preorder Nat

Equations

• Nat.preorder = Preorder.mk Nat.le_refl ⋯ ⋯

instance Nat.partialOrder : PartialOrder Nat

Equations

• Nat.partialOrder = PartialOrder.mk ⋯

instance Nat.totalOrder : TotalOrder Nat

Equations

• Nat.totalOrder = TotalOrder.mk Nat.le_total

instance Nat.WellOrder : WellOrder Nat

Equations

• Nat.WellOrder = WellOrder.mk @Nat.WellOrder.proof_1

theorem Nat.le_one {n : Nat} : n ≤ 1 ↔ n = 0 ∨ n = 1

theorem Nat.one_le_iff_ne_zero {n : Nat} : 1 ≤ n ↔ n ≠ 0

theorem Nat.le_iff_exists_eq_add {n m : Nat} : n ≤ m ↔ ∃ (p : Nat), m = p + n

theorem Nat.le_iff_exists_eq_add' {n m : Nat} : n ≤ m ↔ ∃ (p : Nat), m = n + p

theorem Nat.lt_two_pow {n : Nat} : n < 2 ^ n

theorem Nat.lt_pow_ge_lt {n m : Nat} (h : 2 ≤ n) : m < n ^ m

def Nat.ind_start {motive : Nat → Prop} {start : Nat} (hstart : motive start) (succ : ∀ (n : Nat), start ≤ n → motive n → motive (n + 1)) (n : Nat) : start ≤ n → motive n

Equations

• ⋯ = ⋯

def Nat.ind_start_end {motive : Nat → Prop} {start stp : Nat} (hstart : motive start) (succ : ∀ (n : Nat), start ≤ n → n < stp → motive n → motive (n + 1)) (n : Nat) : start ≤ n → n ≤ stp → motive n

Equations

• ⋯ = ⋯

def Nat.ind_end_start {motive : Nat → Prop} {start stp : Nat} (hstp : motive stp) (succ : ∀ (n : Nat), start ≤ n → n < stp → motive (n + 1) → motive n) (n : Nat) : start ≤ n → n ≤ stp → motive n

Equations

• ⋯ = ⋯

theorem Nat.lt_iff_exists_eq_add' {n m : Nat} : n < m ↔ ∃ (p : Nat), p > 0 ∧ m = n + p

@[simp]

theorem Nat.zero_least : ⊥ = 0

theorem Nat.monotone_of_le_succ {α : Type u_1} [Preorder α] {f : Nat → α} (h : ∀ (n : Nat), f n ≤ f (n + 1)) : Monotone f

theorem Nat.strictMono_of_lt_succ {α : Type u_1} [PartialOrder α] {f : Nat → α} (h : ∀ (n : Nat), f n < f (n + 1)) : StrictMonotone f