ext x
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)
⊢ deriv (f - g) = deriv f - deriv g
case h
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)
x : ℝ
⊢ deriv (f - g) x = (deriv f - deriv g) x