proposition: Lemma rs_gen_is_gen : poly_rV \gen_(a, d) \in 'cgen[Ccode.mk RS_cyclic].
proof: Proof. apply pgen_is_cgen => /=; first exact: RS_not_trivial. apply/forallP => /= p; apply/eqP; apply/idP/idP. move=> Hp. move: (proj1 (rs_genP dn a0 (prim_root_not_uroot_on an) p)). rewrite RS.codebook_syndrome //. rewrite inE mem_kernel_syndrome0 /syndrome in Hp. rewrite Hp => /(_ erefl); case=> m [H1 H2]. rewrite poly_rV_K // ?size_rs_gen //. by rewrite H2 dvdp_mull // modpp. move=> Hp. rewrite inE mem_kernel_syndrome0 /linearcode.syndrome. rewrite -(@RS.codebook_syndrome _ a n' d) //. apply: (proj2 (rs_genP dn a0 (prim_root_not_uroot_on an) p)). rewrite poly_rV_K // ?size_rs_gen // in Hp. case/dvdpP : Hp => x Hx. by exists x; split => //; exact: RS_message_size Hx. 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