proposition: Lemma increasing_on_0_to_half : forall x y, 0 < x <= 1/2 -> 0 < y <= 1/2 -> x <= y -> H2ln x <= H2ln y.
proof: Proof. apply pderive_increasing_open_closed with (pr := pderivable_H2ln); first lra. move=> t [Ht1 Ht2]. rewrite /H2ln /pderivable_H2ln derive_pt_minus 2!derive_pt_mult /=. destruct (Rlt_le_dec 0 t) => /=; last by exfalso; lra. rewrite derive_pt_comp /= mulRA. apply (@leR_trans (- ln t + ln (1 - t))); last first. apply Req_le; field. by split=> ?; lra. rewrite -ln_Rinv // -ln_mult; last 2 first. exact/invR_gt0. lra. rewrite -ln_1. apply ln_increasing_le; first lra. apply (@leR_pmul2l t) => //. by rewrite mulRA mulRV ?gtR_eqF // mulR1 mul1R; lra. Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb