proposition: Lemma RS_syndromep_codeword' t (tr : t < d.+1) (c : 'rV[F]_n) : c \in codebook -> \RSsynp_(rVexp a n, c, t) = 0.
proof: Proof. rewrite inE // => /forallP H. rewrite /syndromep /poly_decoding.syndromep poly_def (eq_bigr \0) ?big1 //. move=> i _. have [:tmp] @j : 'I_d.+1. apply/(Sub i.+1)/(leq_ltn_trans (ltn_ord _)). abstract: tmp. exact tr. by move: (H j) => /= /eqP ->; rewrite scale0r. 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