English
Let P be a property on natural numbers. If P holds for a base point and the step from all larger numbers to n holds, then P holds for all n.
Русский
Пусть P — свойство над натуральными. Если существует основание и условие перехода от любых больших значений к n, то P выполняется для всех n.
LaTeX
$$$\\text{Strong induction: }(\\text{base})\\ (∃n, ∀m>n, P(m))\\; (\\text{step})\\ (∀n, (∀m>n, P(m)) \\to P(n))\\; \\to\\; ∀n, P(n)$$$
Lean4
@[elab_as_elim]
theorem strong_decreasing_induction (base : ∃ n, ∀ m > n, P m) (step : ∀ n, (∀ m > n, P m) → P n) (n : ℕ) : P n :=
by
apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
· intro n ih m hm
rcases hm.eq_or_lt with rfl | hm
· exact step n ih
· exact ih m hm
· rintro ⟨b, hb⟩
rcases base with ⟨n, hn⟩
specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
all_goals cutsat
