proposition: Lemma pderivable_H2ln : pderivable H2ln (fun x => 0 < x <= 1/2).
proof: Proof. move=> x /= [Hx0 Hx1]. apply derivable_pt_minus. apply derivable_pt_mult. apply derivable_pt_Ropp. apply derivable_pt_ln. assumption. apply derivable_pt_mult. apply derivable_pt_Rminus. apply derivable_pt_comp. apply derivable_pt_Rminus. apply derivable_pt_ln_Rminus. lra. Defined.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb