proposition: Lemma prim_pp : forall p, p != 0 -> primitive (pp p).
proof: Proof. by move=> p p0; rewrite /pp; case: (gcdsr_odivp p0)=> x [-> px]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)