proposition: Lemma hamming_MD_alt : MD_decoding_alt hamming_repair C_not_empty.
proof: Proof. rewrite /MD_decoding => /= y c. rewrite /= /hamming_repair ffunE => -[] yc. have : dH y c = O \/ dH y c = 1%nat. rewrite -yc dH_wH. move: (wH_hamming_err_ub y). rewrite leq_eqVlt ltnS leqn0 => /orP[] /eqP; by auto. have c_is_cw : c \in [set cw in Hamming.code m]. by rewrite inE -yc mem_kernel_syndrome0 syndromeD syndrome_hamming_err F2_addmx. case=> [dH0 | dH1]. move: (@leq_bigmin _ _ C_not_empty c c_is_cw (dH y)). by rewrite dH0 leqn0 => /eqP. move: (@leq_bigmin _ _ C_not_empty c c_is_cw (dH y)). rewrite dH1. set x := arg_min _ _ _. rewrite -yc /hamming_repair in dH1. have syndrome_not_0 : syndrome (Hamming.PCM m) y != 0. apply/eqP => syndrome_is_0. move: dH1. by rewrite /hamming_err syndrome_is_0 nat_of_rV_0 addr0 dHE subrr wH0. move=> dHy. suff : dH y x != O. by move: dHy; rewrite leq_eqVlt => /orP[/eqP //|]; rewrite ltnS leqn0 => ->. apply/negP => abs. have : y = x by move: abs; rewrite dHE wH_eq0 subr_eq0 => /eqP. rewrite /x; case: arg_minnP => [|/=]; first by case: C_not_empty. move=> y' Hy' _ yy'; rewrite -{}yy' in Hy'. move/negP : syndrome_not_0; apply. by rewrite -mem_kernel_syndrome0; rewrite inE in Hy'. 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