proposition: Lemma H2_max : forall p, 0 < p < 1 -> H2 p <= 1.
proof: Proof. move=> p [Hp0 Hp1]. rewrite /H2. apply (@leR_pmul2l (ln 2)) => //. rewrite mulR1 mulRDr /log -!mulNR !(mulRC (ln 2)) -!mulRA. rewrite (mulVR _ ln2_neq0) !mulR1 (mulNR (1 - p)); exact/H2ln_max. Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb