proposition: Lemma repair_failure2 e c : c \in lcode -> ~~ (if repair e is Some y0 then y0 != c else true) -> wH (c + e) <= 1.
proof: Proof. move=> Hc H. suff : dH e c = O \/ dH e c = 1%N by rewrite dHE F2_mx_opp addrC; case=> ->. move: H. move x : (repair e) => [|] // ex. rewrite negbK => /eqP xc. move: ex; rewrite {}xc {x}. rewrite /repair /Decoder.repair /= /hamming_repair ffunE; case => <-. move: (wH_hamming_err_ub e). rewrite dH_wH leq_eqVlt ?ltnS ?leqn0 => /orP[|] /eqP ->; by auto. 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