proposition: Lemma fdcoor_GRS_syndrome_coor y l : l < n' -> l < d -> fdcoor b y (inord l.+1) = GRS.syndrome_coord b b l y.
proof: Proof. move=> ln id1. rewrite /fdcoor /GRS.syndrome_coord horner_poly; apply/eq_bigr => /= j _. rewrite insubT // => jn. rewrite 2!mxE -mulrA; congr (y ord0 _ * _); first by apply val_inj. by rewrite -exprS -exprM mulnC exprM inordK. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code