proposition: Lemma syndromepN x : syndromep u (- x) t = - syndromep u x t.
proof: Proof. rewrite /syndromep !poly_def -[RHS]mulN1r big_distrr; apply eq_bigr => /= i _. by rewrite fdcoorN mulN1r scaleNr. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft