proposition: Lemma H_G_T : 'H *m 'G ^T = 0.
proof: Proof. by rewrite -trmx0 -G_H_T trmx_mul trmxK. 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