proposition: Lemma GEN'E : GEN' = GEN''.
proof: Proof. rewrite /GEN' /GEN'' /Syslcode.GEN !F2_mx_opp. Abort. Lemma PCM_GEN' : PCM *m GEN'^T = 0. Proof. rewrite PCM_A_1 /GEN' /= trmx_cast (castmx_cols_mulmx subnK). by rewrite tr_row_mx trmxK mul_row_col tr_scalar_mx mulmx1 mulmxN mul1mx addrN. 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