induction n with
| zero => simp
| succ n h =>
  simp [iteratedDeriv_succ, h]
  ext x
  apply deriv_add
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
  . apply Differentiable.differentiableAt
    exact ContDiff.differentiable_iteratedDeriv _ hg (WithTop.coe_lt_top _)
n : ℕ
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
⊢ iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
no goals