proposition: Lemma mxminpolyP n (A : 'M[F]_n.+1) (p : {poly F}) : p \is monic -> horner_mx A p = 0 -> (forall q, horner_mx A q = 0 -> (dvdp p q)) -> p = mxminpoly A.
proof: Proof. move=> pmon eqpA0 pdvq. apply/eqP; rewrite -eqp_monic //; last exact: mxminpoly_monic. apply/andP; split. by apply/pdvq/mx_root_minpoly. exact: mxminpoly_min. Qed.
imports: mathcomp(all_ssreflect all_algebra)