proposition: Lemma RS_mod_is_GRS_mod y : RS_mod y t = - GRS_mod y (rVexp a n) (rVexp a n) t.
proof: Proof. rewrite /RS_mod /GRS_mod; congr (- _); apply/eq_bigr => /= i iy. rewrite !mulrN scalerN; congr (- _). rewrite -!scalerAl; congr (_ *: _ ). rewrite -mulrA; congr (_ * _). apply eq_big. by move=> j; rewrite in_setD1 andbC. by move=> j; rewrite mxE. by rewrite mxE -polyCM -exprSr -exprM mulnC. 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