proposition: Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p).
proof: Proof. move=> fg; apply: commr_horner => // i. by rewrite coef_map; apply/comm_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)