proposition: Lemma ex_derive_plus : forall (f g : K -> V) (x : K), ex_derive f x -> ex_derive g x -> ex_derive (fun x => plus (f x) (g x)) x.
proof: Proof. intros f g x [df Df] [dg Dg]. exists (plus df dg). now apply is_derive_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv