English
If f is injective and f^{[m]}(a) = f^{[n]}(a), then f^{[m-n]}(a) = a, where subtraction is the natural subtraction with the usual interpretation when m≥n.
Русский
Если f инъективна и f^{[m]}(a) = f^{[n]}(a), тогда f^{[m-n]}(a) = a (с учётом обычного определения m-n).
LaTeX
$$$$\forall f:\alpha\to\alpha,\forall m,n:\mathbb{N},\text{Injective}(f)\Rightarrow (f^{[m]}(a)=f^{[n]}(a) \Rightarrow f^{[m-n]}(a)=a). $$$$
Lean4
theorem iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a :=
by
obtain h | h := Nat.le_total m n
{ simp [Nat.sub_eq_zero_of_le h]
}
{ exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
}