proposition: Lemma H2_max' (x : R): 0 <= x <= 1 -> H2 x <= 1.
proof: Proof. move=> [x_0 x_1]. case: x_0 => [?|<-]; last by rewrite bin_ent_0eq0. case: x_1 => [?|->]; last by rewrite bin_ent_1eq0. exact: H2_max. Qed.
imports: mathcomp(all_ssreflect) Reals Lra ssrR Reals_ext Ranalysis_ext logb