proposition: Lemma decreasing_on_half_to_1 (x y : R) : 1/2 <= x < 1 -> 1/2 <= y < 1 -> x <= y -> H2ln y <= H2ln x.
proof: Proof. move=> Hx Hy xy. rewrite -[X in _ <= X]oppRK leR_oppr. move: x y Hx Hy xy. apply pderive_increasing_closed_open with (pr := pderivable_Ropp_H2ln); first lra. move=> t [Ht1 Ht2]. rewrite /H2ln /pderivable_Ropp_H2ln derive_pt_comp derive_pt_minus 2!derive_pt_mult /=. destruct (Rlt_le_dec 0 t) => /=; last first. 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. suff : ln ( 1 - t) <= ln t by move=> ?; lra. by apply ln_increasing_le; lra. Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb