a n : ℕ
⊢ (succ ∘ succ^[n]) a = succ (a + n)
a n : ℕ
⊢ (succ^[n + 1]) a = a + (n + 1)
rw [Function.iterate_succ', add_succ]
no goals
a n : ℕ
⊢ (succ ∘ succ^[n]) a = succ (a + n)
exact congr_arg _ (succ_iterate a n)