proposition: Lemma Derive_correct f x : ex_derive f x -> is_derive f x (Derive f x).
proof: Proof. intros (l,H). cut (Derive f x = l). intros ; rewrite H0 ; apply H. apply is_derive_unique, H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv