calc
_ = iter f (m + n + 1) a := rfl
_ = iter f (m + n) (f a) := by rw [iter_succ]
_ = iter f m (iter f n (f a)) := by rw [ih]
_ = iter f m (iter f (n + 1) a) := by rw [iter_succ]
case succ
α : Sort u_1
f : α → α
m n : Nat
ih : ∀ (a : α), iter f (m + n) a = iter f m (iter f n a)
a : α
⊢ iter f (m + (n + 1)) a = iter f m (iter f (n + 1) a)
no goals