proposition: Lemma repair_codeword c : c \in lcode -> repair c = Some c.
proof: Proof. rewrite /= /repair /= /hamming_repair ffunE => Hc; congr Some. apply/eqP; by rewrite eq_sym addrC -subr_eq subrr eq_sym err_codeword. 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