have hg' : ContDiff ℝ n (deriv g) := hg.iterate_deriv' n 1
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n✝ n : ℕ
ih :
  ∀ {f g : ℝ → E},
    ContDiff ℝ (↑n) f → ContDiff ℝ (↑n) g → iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g
f g : ℝ → E
hf : ContDiff ℝ (↑(n + 1)) f
hg : ContDiff ℝ (↑(n + 1)) g
hf' : ContDiff ℝ (↑n) (deriv f)
hg' : ContDiff ℝ (↑n) (deriv g)
⊢ iteratedDeriv (n + 1) (f - g) = iteratedDeriv (n + 1) f - iteratedDeriv (n + 1) g