ext x
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)
case succ.h
f g : ℝ → ℝ
hf : ContDiff ℝ ⊤ f
hg : ContDiff ℝ ⊤ g
n : ℕ
h : iteratedDeriv n (f + g) = iteratedDeriv n f + iteratedDeriv n g
x : ℝ
⊢ deriv (iteratedDeriv n f + iteratedDeriv n g) x = (deriv (iteratedDeriv n f) + deriv (iteratedDeriv n g)) x