proposition: Lemma plogp_X (p q : {poly F}) : 2 < size p -> primitive_poly p -> ~~ (p %| q) -> p %| q - 'X ^+ plogp p q.
proof: Proof. move=> sp_gt2 Hh pNDq. rewrite /plogp. case (boolP (primitive_poly p)) => // Hh'; last by case/negP: Hh'. have pM : p \is monic by case/and4P: Hh'. have pMi : monic_irreducible_poly p by apply: primitive_mi. set q' : {poly %/ p with primitive_mi Hh'} := in_qpoly p q. apply/modp_eq0P; rewrite modpD modpN; apply/eqP; rewrite subr_eq0; apply/eqP. rewrite !Pdiv.IdomainMonic.modpE //=. suff /val_eqP/eqP/= : 'qX ^+ qlogp q' = q'. rewrite /= [X in rmodp _ X]mk_monicE // => <-. by rewrite poly_of_qpolyX /= mk_monicE // [rmodp 'X p]rmodp_small ?size_polyX. apply: qlogp_qX => //. apply/eqP=> /val_eqP/eqP. rewrite /= mk_monicE // => /rmodp_eq0P; rewrite -dvdpE => pDq. by case/negP: pNDq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)