proposition: Lemma f0 a b : 0 <= f a b.
proof: Proof. rewrite /f ffunE. case: b => [a'|]; last first. by case: p_01 => /RleP. case: ifP => _ //. case: p_01 => ? ? //. exact/onem_ge0/RleP. Qed.
imports: mathcomp(all_ssreflect all_algebra matrix) Reals mathcomp(mathcomp_extra Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy binary_entropy_function channel hamming channel_code