proposition: Lemma fdcoor_syndrome_coord (y : 'rV['F_2]_n) i (it : i < t.*2) : fdcoor (rVexp a n) (F2_to_GF2 m y) (inord i.+1) = GRS.syndrome_coord (rVexp a n) (rVexp a n) i (F2_to_GF2 m y).
proof: Proof. rewrite /fdcoor /GRS.syndrome_coord horner_poly; apply eq_bigr => j _. rewrite insubT // => jn. rewrite !mxE -mulrA; congr (GF2_of_F2 (y _ _) * _); first by apply val_inj. by rewrite -exprS -exprM mulnC exprM inordK // ltnS (leq_trans it). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2