proposition: Lemma bsc_out_H_half' : 0 < 1%:R / 2%:R < 1.
proof: Proof. rewrite /= (_ : 1%:R = 1) // (_ : 2%:R = 2) //. split => //. apply: divR_gt0 => //. apply/ltR_pdivr_mulr => //. by rewrite mul1R. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum zmodp matrix lra) mathcomp(mathcomp_extra classical_sets Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist entropy binary_entropy_function channel hamming channel_code pproba