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