proposition: Lemma repair_failure1 e c : c \in lcode -> (if repair e is Some x then x != c else true) -> 1 < wH (c + e).
proof: Proof. move=> Hc. move xc : (repair e) => [x ex |]; last first. by move=> _; move: xc; rewrite /repair /= /hamming_repair ffunE. rewrite ltnNge; apply: contra xc. rewrite leq_eqVlt ltnS leqn0 orbC => /orP[|/eqP cy1]. - rewrite wH_eq0 => /eqP/F2_addmx0 cy. by move: ex; rewrite -cy repair_codeword // => -[->]. - move: (ex); rewrite (@encode_decode _ e Hc) ?ex // ?dHE // ?F2_mx_opp ?cy1 //. by case => ->. 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