proposition: Lemma continuous_ln x : (0 < x) -> continuous ln x.
proof: Proof. move => Hxgt0. apply: ex_derive_continuous. exists (/x). apply is_derive_Reals. exact: derivable_pt_lim_ln. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp