proposition: Lemma derivable_pt_ln_Rminus x : x < 1 -> derivable_pt ln (1 - x).
proof: Proof. move=> Hx. exists (/ (1 - x)). apply derivable_pt_lim_ln, subR_gt0. assumption. Defined.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb