apply Differentiable.differentiableAt
case succ.h.hf
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ DifferentiableAt ℝ (fun y => iteratedDeriv n f y) x
case succ.h.hf.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ Differentiable ℝ fun y => iteratedDeriv n f y