proposition: Lemma derivable_pt_Log b x : 0 < x -> derivable_pt (Log b) x.
proof: Proof. move=> x0. exists (/ln b * / x). apply derivable_pt_lim_Log. assumption. Defined.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext