proposition: Lemma horner_errloc_0 (a : 'rV[F]_n) E : (errloc a E).[0] = 1.
proof: Proof. rewrite /errloc horner_prod (eq_bigr (fun=> 1)) ?big1_eq //. by move=> /= j _; rewrite !hornerE subr0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft