proposition: Lemma is_derive_n_plus (f g : R -> R) (n : nat) (x lf lg : R) : locally x (fun y => forall k, (k <= n)%nat -> ex_derive_n f k y) -> locally x (fun y => forall k, (k <= n)%nat -> ex_derive_n g k y) -> is_derive_n f n x lf -> is_derive_n g n x lg -> is_derive_n (fun x => f x + g x) n x (lf + lg).
proof: Proof. case: n x lf lg => /= [ | n] x lf lg Hfn Hgn Hf Hg. by rewrite Hf Hg. apply is_derive_ext_loc with (fun y => Derive_n f n y + Derive_n g n y). apply locally_locally in Hfn. apply locally_locally in Hgn. generalize (filter_and _ _ Hfn Hgn). apply filter_imp => {Hfn Hgn} y [Hfn Hgn]. apply sym_eq, Derive_n_plus. apply filter_imp with (2 := Hfn) ; by intuition. apply filter_imp with (2 := Hgn) ; by intuition. by apply: is_derive_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv