proposition: Lemma encode_code pt : encode pt \in kernel 'H.
proof: Proof. rewrite memv_ker lfunE /= /encode ffunE /syndrome. by rewrite trmx_mul trmxK -mulmxA G_H_T mulmx0. 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