proposition: Lemma plogp_lt (p q : {poly F}) : 2 < size p -> plogp p q < #|{poly %/ p}|.-1.
proof: Proof. move=> /ltnW size_gt1. rewrite /plogp. case (boolP (primitive_poly p)) => // Hh; first by apply: qlogp_lt. by rewrite ltn_predRL (card_finRing_gt1 {poly %/ p}). 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)