proposition: Lemma mxminpoly_minP p : reflect (horner_mx A p = 0) (p_A %| p).
proof: Proof. apply: (iffP idP); last exact: mxminpoly_min. by move=> /Pdiv.Field.dvdpP[q ->]; rewrite rmorphM/= mx_root_minpoly mulr0. 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)