proposition: Lemma syndomepE r y : syndromep r y = \sum_(i in supp y) (y ``_ i * b ``_ i)%:P * (\sum_(l < r) (a ``_ i ^+ l)%:P * 'X^l).
proof: Proof. rewrite /syndromep poly_def. rewrite (eq_bigr (fun i : 'I_r=> 'X^i * (syndrome_coord i y)%:P)); last first. by move=> i _; rewrite mulrC -scale_polyE. rewrite (eq_bigr (fun i : 'I_r => 'X^i * (syndrome_coord_supp i y)%:P)); last first. move=> i _. by rewrite syndrome_coord_suppE. rewrite /syndrome_coord_supp. rewrite (eq_bigr (fun i : 'I_r => (\sum_(j in supp y) 'X^i * (y ``_ j * b ``_ j * a ``_ j ^+ i)%:P))); last first. move=> i _. by rewrite -big_distrr /= (big_morph (id1:=0) (fun x => x%:P) (@polyCD _)). rewrite exchange_big /=. rewrite (eq_bigr (fun j => (y ``_ j * b ``_ j)%:P * \sum_(l < r) ((a ``_ j ^+ l)%:P * 'X^l))) //. move=> i isupp. rewrite !big_distrr /=; apply eq_bigr => j _. by rewrite mulrC mulrA polyCM. 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