induction n with
| zero => simp
| succ n h =>
  conv => rhs; rw [iteratedDeriv_succ]
  rw [iteratedDeriv_succ]
  rw [h]
  ext x
  conv => lhs; arg 1; intro x
  simp [deriv_const_mul]
n : ℕ
r : ℝ
f : ℝ → ℝ
⊢ iteratedDeriv n (r • f) = r • iteratedDeriv n f
no goals