proposition: Lemma EC_non_flip (a : X) (i : option X): (i != None) && (i != Some a) -> 0 = EC.f p a i.
proof: Proof. case: i => //= x xa; rewrite ffunE; case: ifP => // ax; move: xa. by rewrite (eqP ax) eqxx. 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