proposition: Lemma plogp1 (p : {poly F}) : 2 < size p -> plogp p 1 = 0%N.
proof: Proof. move=> sp_gt2; rewrite /plogp; case (boolP (primitive_poly p)) => // i. suff->: in_qpoly p 1 = 1 by apply: qlogp1. apply/val_eqP/eqP; apply: in_qpoly_small. rewrite mk_monicE ?size_poly1 ?(leq_trans _ sp_gt2) //. by apply: primitive_mi. 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)