proposition: Lemma mx_discardE : mx_discard = mx_discard'.
proof: Proof. apply/matrixP => a b. rewrite /mx_discard /mx_discard' /Syslcode.DIS !castmxE /= cast_ord_id. Abort. Lemma mx_discard_GEN' : mx_discard *m GEN'^T = 1%:M. Proof. rewrite /GEN' /mx_discard /= trmx_cast (castmx_cols_mulmx subnK). rewrite tr_row_mx trmxK mul_row_col. by rewrite tr_scalar_mx mulmx1 mul0mx addr0. 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