proposition: Lemma is_derive_ln x : 0 < x -> is_derive ln x (/ x)%R.
proof: Proof. move=> H; exact/is_derive_Reals/derivable_pt_lim_ln. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp