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