proposition: Lemma RS_syndromep_codeword (c : 'rV[F]_n) : (\RSsynp_(rVexp a n, c, d) == 0) = (c \in codebook).
proof: Proof. apply/idP/idP => [/eqP | ]; last first. by move/(@RS_syndromep_codeword' d) => /(_ (ltnSn _)) ->. rewrite codebook_syndrome syndrome_syndromep => /eqP ?. by rewrite poly_rV_0. 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