proposition: Lemma pderivable_log a x1 : 0 <= a -> pderivable log (fun x2 : R => a < x2 < x1).
proof: Proof. move=> a0; rewrite /pderivable => x Hx. rewrite /log /Log (_ : (fun x0 => ln x0 / ln 2) = (mult_real_fct (/ ln 2) (fun x0 => ln x0))); last first. by rewrite boolp.funeqE => x0; rewrite /mult_real_fct mulRC. apply/derivable_pt_scal/derivable_pt_ln/(leR_ltR_trans a0); by case: Hx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex