English
Iterating the predecessor n times yields subtraction by n: pred^{[n]}(x) = x − n.
Русский
Повторное применение предшественника n раз даёт вычитание на n: pred^{[n]}(x) = x − n.
LaTeX
$$$\\\\mathrm{pred}^{[n]}(x) = x - n.$$$
Lean4
@[simp]
theorem pred_iterate [AddCommGroupWithOne α] [PredSubOrder α] (x : α) (n : ℕ) : pred^[n] x = x - n := by
induction n with
| zero => rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
| succ n IH => rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]