English
There is an induction principle for structures with a PredOrder, mirroring Succ.rec in the dual setting.
Русский
Существует принцип индукции для структур с PredOrder, зеркально отражающий Succ.rec в двойственной настройке.
LaTeX
$$Pred.rec expresses induction along decreasing chains using pred.$$
Lean4
/-- Induction principle on a type with a `PredOrder` for all elements below a given element `m`. -/
@[elab_as_elim]
theorem rec {m : α} {P : ∀ n, n ≤ m → Prop} (rfl : P m le_rfl)
(pred : ∀ n (hnm : n ≤ m), P n hnm → P (pred n) ((pred_le _).trans hnm)) ⦃n : α⦄ (hnm : n ≤ m) : P n hnm :=
Succ.rec (α := αᵒᵈ) (P := P) rfl pred hnm
