English
If the n-th iterate of succ at a equals the m-th iterate and n < m, then the n-th iterate is maximal.
Русский
Если n-ая и m-ая итерации succ совпадают и n < m, то n-ая итерация является максимальной.
LaTeX
$$$\\forall a:\\alpha\\,\\forall n,m:\\mathbb{N},\\ (\\operatorname{iterate}(\\operatorname{succ}, n)a = \\operatorname{iterate}(\\operatorname{succ}, m)a) \\land n < m \\Rightarrow \\mathrm{IsMax}(\\operatorname{iterate}(\\operatorname{succ}, n)a)$$$
Lean4
theorem isMax_iterate_succ_of_eq_of_lt {n m : ℕ} (h_eq : succ^[n] a = succ^[m] a) (h_lt : n < m) : IsMax (succ^[n] a) :=
by
refine max_of_succ_le (le_trans ?_ h_eq.symm.le)
rw [← iterate_succ_apply' succ]
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le
