proposition: Lemma mx_discard_GEN : mx_discard *m GEN ^T = 1%:M.
proof: Proof. rewrite /GEN /mx_discard tr_col_perm -mul_col_perm. rewrite -col_permM. have -> : (systematic * systematic^-1 = 1)%g. apply/permP=> i. by rewrite permM permK perm1. by rewrite col_perm1 SysHamming.mx_discard_GEN'. 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