proposition: Lemma Derive_plus : forall f g x, ex_derive f x -> ex_derive g x -> Derive (fun x => f x + g x) x = Derive f x + Derive g x.
proof: Proof. intros f g x Df Dg. apply is_derive_unique. apply: is_derive_plus ; now apply Derive_correct. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv