proposition: Lemma minPoly_dvdp p : p \is a polyOver K -> root p x -> (minPoly K x) %| p.
proof: Proof. move=> Kp rootp. have gcdK : gcdp (minPoly K x) p \is a polyOver K. by rewrite gcdp_polyOver ?minPolyOver. have /orP[gcd_eqK|gcd_eq1] := minPoly_irr gcdK (dvdp_gcdl (minPoly K x) p). by rewrite -(eqp_dvdl _ gcd_eqK) dvdp_gcdr. case/negP: (root1 x). by rewrite -(eqp_root gcd_eq1) root_gcd rootp root_minPoly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)