proposition: Lemma syndromepE y : syndromep u y t = \sum_(j in supp y) \sum_(i < t) (y ``_ j * u ``_ (inord i.+1) ^+ j) *: 'X^i.
proof: Proof. rewrite /syndromep exchange_big /= poly_def; apply/eq_bigr => i _; rewrite /fdcoor horner_poly. rewrite (bigID (fun i => i \in supp y)) /= -[RHS]addr0 scalerDl; congr (_ + _). rewrite scaler_suml; apply/eq_bigr => j Hj. rewrite insubT // => H; congr ((y ord0 _ * _) *: _); by apply val_inj. apply/eqP; rewrite scaler_eq0 (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 ?eqxx //. move=> j Hj; rewrite insubT // => H; rewrite (_ : Sub _ _ = j); last by apply/val_inj. move: Hj; rewrite inE negbK => /eqP ->; by rewrite mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft