proposition: Lemma horner_mxZ : scalable horner_mx.
proof: Proof. move=> a p /=; rewrite -mul_polyC rmorphM /=. by rewrite horner_mx_C [_ * _]mul_scalar_mx. 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)