proposition: Lemma fdcoorE y i : y ^`_ i = \sum_(j < n) (y ``_ j) * (u ``_ i) ^+ j.
proof: Proof. rewrite /fdcoor horner_poly; apply eq_bigr => j _; rewrite insubT //= => jn. rewrite (_ : Ordinal jn = j) //; by apply/val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming