proposition: Lemma hamming_err_enc m : hamming_err (f m) = 0.
proof: Proof. by rewrite /hamming_err Hamming'.syndrome_enc 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