proposition: Lemma ex_derive_is_derive : forall (f : R -> R) x l, is_derive f x l -> ex_derive f x.
proof: Proof. move=> f x l; rewrite /is_derive_n /ex_derive_n => H. eexists; exact: H. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp