proposition: Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B.
proof: Proof. by move=> ?; apply/comm_mx_sym/comm_mx_horner/comm_mx_sym. 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)