proposition: Lemma derivable_pt_ln x : 0 < x -> derivable_pt ln x.
proof: Proof. move=> Hx; exists (/ x); apply derivable_pt_lim_ln; assumption. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext