proposition: Lemma G_H_T : 'G *m 'H ^T = 0.
proof: Proof. rewrite /GEN /PCM trmx_cast /= (castmx_cols_mulmx subnKC) tr_row_mx. by rewrite mul_row_col mul1mx trmx1 mulmx1 -linearD addrN linear0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code