proposition: Lemma RS_cyclic : rcsP [set cw in RS.code a n d].
proof: Proof. rewrite (_ : [set cw in _] = [set cw in RS.codebook a n' d]); last first. apply/setP => i; by rewrite -RS.lcode0_codebook // inE 2![in RHS]inE. move=> /= y. rewrite !inE => /forallP x_RS. apply/forallP => /= i; apply/implyP => i0; apply/eqP. move: x_RS => /(_ i); rewrite i0 implyTb => /eqP x_RS. move/(congr1 (fun x => a^+i * x)) : x_RS. rewrite mulr0 => H. apply fdcoor_rcs; first exact: prim_expr_order. move/eqP: H. by rewrite mulf_eq0 expf_eq0 i0 (negbTE a0) /= => /eqP. 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