no goals
α : Type u
β : Type v
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]
simp only [Nat.mul_zero, iterate_zero]
no goals
α : Type u
β : Type v
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]
simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]