Theorems · Theorem · order theory

Nat.le_induction

∀ {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop},
  P m ⋯ → (∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) → ∀ (n : ℕ) (hmn : m ≤ n), P n hmn

Induction principle starting at a non-zero number. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction'). This is an alias of Nat.leRec, specialized to Prop.

Defined in

Mathlib.Data.Nat.Init

Cited by

46 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms