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.neg']
n : ℕ
f : ℝ → ℝ
⊢ iteratedDeriv n (-f) = -iteratedDeriv n f
no goals