a n : ℕ
⊢ (pred ∘ pred^[n]) a = pred (a - n)
a n : ℕ
⊢ (pred^[n + 1]) a = a - (n + 1)
rw [Function.iterate_succ', sub_succ]
no goals
a n : ℕ
⊢ (pred ∘ pred^[n]) a = pred (a - n)
exact congr_arg _ (pred_iterate a n)