proposition: Lemma evaluateE p : evaluate p = \row_(i < d) p.[points`_i].
proof: Proof. apply/rowP => i; rewrite !mxE horner_coef /=. by apply: eq_big => // j _; rewrite !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)