proposition: Lemma horner_rVpoly m (u : 'rV_m) : horner_mx (rVpoly u) = vec_mx (u *m powers_mx m).
proof: Proof. rewrite mulmx_sum_row linear_sum [rVpoly u]poly_def rmorph_sum. apply: eq_bigr => i _. by rewrite valK /= !linearZ rmorphXn /= horner_mx_X rowK /= mxvecK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)