proposition: Lemma plogp_div_eq0 (p q : {poly F}) : 2 < size p -> (p %| q) -> plogp p q = 0%N.
proof: Proof. move=> sp_gt2; rewrite /plogp; case (boolP (primitive_poly p)) => // i pDq. suff-> : in_qpoly p q = 0 by apply: qlogp0. by apply/eqP; rewrite primitive_poly_in_qpoly_eq0. 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)