W1.iteratedDeriv_sub

lemma iteratedDeriv_sub {f g : ℝ → E} (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) :    iteratedDeriv n (f - g) = iteratedDeriv n f - iteratedDeriv n g := by  induction n generalizing f g with  | zero => rfl  | succ n ih =>    have hf' : ContDiff ℝ n (deriv f) := hf.iterate_deriv' n 1    have hg' : ContDiff ℝ n (deriv g) := hg.iterate_deriv' n 1    have hfg : deriv (f - g) = deriv f - deriv g := by      ext x ; apply deriv_sub      · exact (hf.differentiable (by simp)).differentiableAt      · exact (hg.differentiable (by simp)).differentiableAt    simp_rw [iteratedDeriv_succ', ← ih hf' hg', hfg]