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