proposition: Lemma minPoly_irr p : p \is a polyOver K -> p %| minPoly K x -> (p %= minPoly K x) || (p %= 1).
proof: Proof. rewrite dvdp_eq; set q := _ %/ _ => Kp def_pq. have Kq: q \is a polyOver K by rewrite divp_polyOver // minPolyOver. move: q Kq def_pq root_minPoly (size_minPoly K x) => q Kq /eqP->. rewrite rootM => pqx0 szpq. have [nzq nzp]: q != 0 /\ p != 0. by apply/norP; rewrite -mulf_eq0 -size_poly_eq0 szpq. without loss{pqx0} qx0: q p Kp Kq nzp nzq szpq / root q x. move=> IH; case/orP: pqx0 => /IH{}IH; first exact: IH. have{IH} /orP[]: (q %= p * q) || (q %= 1) by apply: IH => //; rewrite mulrC. by rewrite orbC -{1}[q]mul1r eqp_mul2r // eqp_sym => ->. by rewrite -{1}[p]mul1r eqp_sym eqp_mul2r // => ->. apply/orP; right; rewrite -size_poly_eq1 eqn_leq lt0n size_poly_eq0 nzp andbT. rewrite -(leq_add2r (size q)) -leq_subLR subn1 -size_mul // mulrC szpq. by rewrite ltnNge; apply: contra nzq => /(root_small_adjoin_poly Kq) <-. 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)