proposition: Lemma plogpD (p q1 q2 : {poly F}) : 2 < size p -> primitive_poly p -> ~~ (p %| q1) -> ~~ (p %| q2) -> plogp p (q1 * q2) = ((plogp p q1 + plogp p q2) %% #|{poly %/ p}|.-1)%N.
proof: Proof. move=> sp_gt2 Pp pNDq1 pNDq2. rewrite /plogp; case (boolP (primitive_poly p)) => [|/negP//] i /=. have pmi := primitive_mi i. by rewrite rmorphM qlogpD //= 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)