proposition: Lemma BCH_mod_is_GRS_mod y : BCH_mod y = GRS_mod y (rVexp a n) (rVexp a n) t.*2.
proof: Proof. rewrite /BCH_mod /GRS_mod; apply/eq_bigr => i iy. rewrite !mulrN scalerN; congr (- _). rewrite -!scalerAl; congr (_ *: _). rewrite mxE -mulrA; congr (_ * _). apply/eq_big. by move=> j; rewrite in_setD1 andbC. move=> j _; by rewrite mxE. by rewrite -polyCM -exprSr -exprM mulnC. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2