. apply Differentiable.differentiableAt
  exact ContDiff.differentiable_iteratedDeriv _ hf (WithTop.coe_lt_top _)
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.hg
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 g y) x
case succ.h.hg
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 g y) x