proposition: Lemma MD_BDD (Himg : oimg f \subset C) : (forall x, f x != None) -> MD_decoding [set cw in C] f -> (mdd_err_cor C_not_trivial).-BDD (C, f).
proof: Proof. move=> no_fail Hmin. rewrite /BD_decoding => /= c e cC wHe. move: (@mddP _ _ _ _ Hmin C_not_trivial Himg c (c + e) (no_fail _) cC) => //. by rewrite dH_wH => /(_ wHe). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code