conv => rhs; rw [iteratedDeriv_succ]
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -iteratedDeriv (Nat.succ n) f
case succ
f : ℝ → ℝ
n : ℕ
h : iteratedDeriv n (-f) = -iteratedDeriv n f
⊢ iteratedDeriv (Nat.succ n) (-f) = -deriv (iteratedDeriv n f)