simp [iteratedDeriv_succ, h]
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ iteratedDeriv (Nat.succ n) (f + g) = iteratedDeriv (Nat.succ n) f + iteratedDeriv (Nat.succ n) g
case succ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) = deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)