proposition: Lemma err_codeword c : c \in lcode -> hamming_err c = 0.
proof: Proof. rewrite /hamming_err mem_kernel_syndrome0 => /eqP ->; by rewrite nat_of_rV_0. 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