proposition: Lemma submod_closed : submod_closed codebook.
proof: Proof. split=> [|k x y xC yCby]; first exact: O_in_codebook. by rewrite (proj2 addr_closed) // scaler_closed. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code