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