proposition: Lemma H2ln_max (q : R) : 0 < q < 1 -> - q * ln q - (1 - q) * ln (1 - q) <= ln 2.
proof: Proof. move=> [Hq0 Hq1]. apply (@leR_trans (H2ln (1/2))); last first. apply Req_le. rewrite /H2ln (_ : 1 - 1/2 = 1/2); last by field. rewrite -mulRBl (_ : - _ - _ = - 1); last by field. rewrite div1R ln_Rinv; [by field | lra]. rewrite -/(H2ln q). case: (Rlt_le_dec q (1/2)) => [H1|]. - by apply increasing_on_0_to_half => //; lra. - case/Rle_lt_or_eq_dec => [H1|<-]; last first. lra. by apply decreasing_on_half_to_1 => //; lra. Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb