proposition: Lemma syndromep_syndrome r y : (syndrome r y == 0) = (syndromep r y == 0).
proof: Proof. apply/idP/idP; rewrite /syndrome /syndromep => H0. apply/eqP/polyP => i. rewrite coef0 coef_poly; case: ifPn => // ir. by move/eqP/rowP : H0 => /(_ (Ordinal ir)); rewrite !mxE. apply/eqP/rowP => i. rewrite mxE. move/eqP/polyP : H0 => /(_ i); rewrite coef0 coef_poly (ltn_ord i) => ->. by rewrite mxE. 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