proposition: Lemma GRS_key_equation r : Sigma * GRS.syndromep a b r y = Omega + GRS_mod r * 'X^r.
proof: Proof. case/boolP : (r == O) => r0. rewrite (eqP r0) mulr1. rewrite /GRS.syndromep poly_def big_ord0 mulr0. apply/eqP; rewrite eq_sym addr_eq0; apply/eqP. rewrite /GRS_mod /Omega /erreval -sumrN; apply eq_bigr => j jy. rewrite expr0 mulr1 mulrN opprK [in RHS]mulrC mulrC -!scalerA. rewrite -scalerAl mulrC mul_polyC; congr (_ *: (_ *: _)). apply eq_bigl => k; by rewrite in_setD1 andbC. rewrite /GRS_mod big_distrl /= /Omega /erreval -big_split /=. rewrite GRS.syndomepE big_distrr /=. apply eq_bigr => i iy. rewrite -3!scalerAl -scalerA -scalerDr. rewrite polyCM -!mulrA mulrCA !mulrA mul_polyC -!scalerAl; congr (_ *: _). rewrite /Sigma /errloc (bigD1 i) //= mulrC -!mulrA mulrBl mul1r. set x := (X in _ * X = _). rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first. rewrite /x mulrCA -mulrBr big_distrr /= -sumrB. rewrite (_ : \sum_(i0 < r) _ = 1 - ((a ``_ i ^+ r)%:P * 'X^r)) //. rewrite big_split /=. destruct r => //. rewrite big_ord_recl /= expr0 mulr1 big_ord_recr /= -addrA. rewrite (addrA _ _ (- (_ *: _ * _))). rewrite addrCA [X in X + _](_ : _ = 0) ?add0r; last first. rewrite sumrN. apply/eqP; rewrite subr_eq0; apply/eqP. apply eq_bigr => j _. rewrite -!scalerAl mulrCA -exprS !scalerAl; congr (_ * _). by rewrite -mul_polyC -polyCM -exprS. by rewrite -mulrCA -scalerAl -exprS 2!mul_polyC scalerA -exprSr. rewrite mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _). apply/eq_bigl => j; by rewrite in_setD1 andbC. rewrite -mulNr !mulrA; congr (_ * _). by rewrite -mulNr -mulrA mulrC -!mulrA. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext vandermonde linearcode dft poly_decoding