proposition: Lemma minpoly_mxM B C : (B \in Ad -> C \in Ad -> B * C \in Ad)%MS.
proof: Proof. move=> AdB AdC; rewrite -(mx_inv_hornerK AdB) -(mx_inv_hornerK AdC). by rewrite -rmorphM ?horner_mx_mem. 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)