proposition: Lemma plogp0 (p : {poly F}) : 2 < size p -> plogp p 0 = 0%N.
proof: Proof. move=> sp_gt2; rewrite /plogp; case (boolP (primitive_poly p)) => // i. by rewrite in_qpoly0 qlogp0. 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)