proposition: Lemma continuous_exp x : continuous exp x.
proof: Proof. apply: ex_derive_continuous. apply: ex_derive_Reals_1. exact: derivable_pt_exp. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp