proposition: Lemma ex_derive_n_plus (f g : R -> R) (n : nat) (x : 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) -> ex_derive_n (fun x => f x + g x) n x.
proof: Proof. case: n x => /= [ | n] x Hf Hg. by []. apply ex_derive_ext_loc with (fun y => Derive_n f n y + Derive_n g n y). apply locally_locally in Hf. apply locally_locally in Hg. generalize (filter_and _ _ Hf Hg). apply filter_imp => {Hf Hg} y [Hf Hg]. apply sym_eq, Derive_n_plus. apply filter_imp with (2 := Hf) ; by intuition. apply filter_imp with (2 := Hg) ; by intuition. apply: ex_derive_plus. apply locally_singleton ; apply filter_imp with (2 := Hf) => {Hf} y Hy ; by apply (Hy (S n)). apply locally_singleton ; apply filter_imp with (2 := Hg) => {Hg} y Hy ; by apply (Hy (S n)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv