proposition: Lemma is_derive_plus : forall (f g : K -> V) (x : K) (df dg : V), is_derive f x df -> is_derive g x dg -> is_derive (fun x => plus (f x) (g x)) x (plus df dg).
proof: Proof. intros f g x df dg Df Dg. eapply filterdiff_ext_lin. apply filterdiff_plus_fct ; try eassumption. simpl => y. by rewrite scal_distr_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv