proposition: Lemma syndrome_coord_suppE l y : syndrome_coord l y = syndrome_coord_supp l y.
proof: Proof. rewrite /syndrome_coord (bigID (fun i => i \in supp y)) /=. rewrite addrC (eq_bigr (fun=> 0)); last first. by move=> i; rewrite inE negbK => /eqP ->; rewrite 2!mul0r. by rewrite big_const iter_addr0 add0r. 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