fact: Variables (M : finType) (n : nat) (f : encT [finType of 'F_2] M n).
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