proposition: Lemma hamming_MD_decoding : MD_decoding [set cw in Hamming.code m] hamming_repair.
proof: Proof. apply (@MD_decoding_equiv _ _ _ hamming_repair C_not_empty). apply/subsetP => x Hx; rewrite inE. by move/subsetP : hamming_repair_img => /(_ _ Hx). by apply hamming_MD_alt. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel