proposition: Lemma repair_failure e c : c \in lcode -> (if repair e is Some x then x != c else true) = (1 < wH (c + e)).
proof: Proof. move=> Hc. apply/idP/idP; first by move/repair_failure1; apply. apply: contraTT; move/repair_failure2; rewrite -leqNgt; by apply. 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