proposition: Lemma is_derive_n_minus (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. move => Hf Hg Df Dg. apply is_derive_n_plus. by []. move: Hg ; apply filter_imp => y Hg k Hk. apply ex_derive_n_opp ; by apply Hg. by []. by apply is_derive_n_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv