proposition: Lemma derivable_pt_lim_Log b (x : R) : 0 < x -> derivable_pt_lim (Log b) x (/ ln b * / x).
proof: Proof. move=> x0. rewrite (_ : Log b = comp (fun x => x / ln b) ln); last by rewrite boolp.funeqE. apply derivable_pt_lim_comp; first exact: derivable_pt_lim_ln. move=> e e0. exists (mkposreal _ e0) => h h0 /= he. rewrite [_ / ln b]/Rdiv mulRDl -(addR_opp _ (ln x / ln b)) addRAC addR_opp. rewrite subRR add0R {1}/Rdiv mulRAC mulRV ?mul1R ?subRR ?normR0 //; exact/eqP. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext