proposition: Lemma encode_image_code (x : 'rV_n) : {y : 'rV_k | Encoder.enc (Lcode.enc C) y = x} -> x \in C.
proof: Proof. case=> y <-. by rewrite /= memv_ker lfunE /= /syndrome ffunE trmx_mul trmxK -mulmxA Syslcode.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