proposition: Lemma rs_gen_is_pgen : \gen_(a, d) \in 'pgen[RS.codebook a n' d].
proof: Proof. apply/forallP => cw; apply/eqP; apply/idP/idP. case/rs_genP => x [sz_x ->]; by rewrite dvdp_mulIr. rewrite dvdp_eq => /eqP H; apply/rs_genP. exists (rVpoly cw %/ \gen_(a, d)); split => //. rewrite size_divp ?gen_neq0 // size_rs_gen. by rewrite -subnS /= leq_sub2r // size_poly. 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