English
There is an induction principle along the successor chain for all elements above a fixed base.
Русский
Существует принцип индукции вдоль последовательности потомков для всех элементов выше заданной основы.
LaTeX
$$Induction along succ: P(n) holds for all n ≥ m if it holds for m and is preserved by succ.$$
Lean4
/-- Induction principle on a type with a `SuccOrder` for all elements above a given element `m`. -/
@[elab_as_elim]
theorem rec {m : α} {P : ∀ n, m ≤ n → Prop} (rfl : P m le_rfl)
(succ : ∀ n (hmn : m ≤ n), P n hmn → P (succ n) (hmn.trans <| le_succ _)) ⦃n : α⦄ (hmn : m ≤ n) : P n hmn :=
by
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate
induction n with
| zero => exact rfl
| succ n ih =>
simp_rw [Function.iterate_succ_apply']
exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)
