proposition: Lemma dvdrp_primr : forall p q, p %| q -> primitive q -> primitive p.
proof: Proof. move=> p q. have [-> | p0] := eqVneq p 0; first by rewrite dvd0r => /eqP->. rewrite /primitive /eqd=> pq ppq; rewrite dvd1r andbT; apply/dvdrP. move: (pp_inj_dvdr pq)=> pppq; rewrite dvdrp_spec in pq. case/andP: pq; case/dvdrP=> x Hx; case/dvdrP=> y Hy. case/andP: ppq; case/dvdrP=> z Hz _. by exists (z * x); rewrite -mulrA -Hx -Hz. 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)