English
Strong induction principle on ℕ+, with n = 1 treated separately.
Русский
Сильный принцип математной индукции на ℕ+, n=1 выделен как базовый случай.
LaTeX
$$$\\\\forall p : \\\\mathbb{N}^+ \\\\to \\\\mathrm{Sort}, \\\\ a \\\\in \\\\mathbb{N}^+, \\\\ p 1 \\\\to \\\\big( \\\\forall n, (\\\\forall m \\\\le n, \\\\ p m) \\\\to \\\\ p(n+1) ) \\\\to \\\\ p a.$$$
Lean4
/-- Strong induction on `ℕ+`, with `n = 1` treated separately. -/
def caseStrongInductionOn {p : ℕ+ → Sort*} (a : ℕ+) (hz : p 1) (hi : ∀ n, (∀ m, m ≤ n → p m) → p (n + 1)) : p a :=
by
apply strongInductionOn a
rintro ⟨k, kprop⟩ hk
rcases k with - | k
· exact (lt_irrefl 0 kprop).elim
rcases k with - | k
· exact hz
exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (Nat.lt_succ_iff.2 hm)
