proposition: Lemma MD_decoding_equiv : MD_decoding_alt <-> MD_decoding.
proof: Proof. split => [H /= y x yx x' x'C | H /= y x yx]. - move: {H}(H _ _ yx) => H. rewrite dH_sym H dH_sym. case: arg_minnP; first by case: c_not_empty. move=> /= i ic ij; by rewrite dH_sym (dH_sym x') ij. - move: {H}(H _ _ yx) => H. case: arg_minnP; first by case: c_not_empty. move=> /= i Hi /(_ x) Ki. apply/eqP; rewrite eqn_leq; apply/andP; split. - by rewrite dH_sym (dH_sym y) H. - apply/Ki; move/subsetP: f_img; apply; rewrite inE. by apply/existsP; exists y; apply/eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup finalg perm) mathcomp(zmodp matrix vector order) mathcomp(lra mathcomp_extra Rstruct reals) Reals ssrR realType_ext Reals_ext ssr_ext ssralg_ext f2 fdist proba channel_code channel binary_symmetric_channel hamming pproba