proposition: Lemma dvdrp_prim_mull : forall a p q, a != 0 -> primitive q -> p %| a%:P * q = (gcdsr p %| a) && (pp p %| q).
proof: Proof. move=> a p q a0 pq; case/andP: (pq)=> pq1 pq2. rewrite dvdrp_spec. case/andP: (gcdsr_mull a q)=> Hg2 Hg3. case/andP: (pp_mul (a%:P) q)=> pp1 pp2. apply/idP/idP; case/andP=> H Hpp. move: (dvdr_mul pq1 (dvdrr a)); rewrite mulrC. move/(dvdr_trans (dvdr_trans H Hg2)); rewrite mul1r=>-> /=. rewrite (dvdr_trans _ (pp_dvdr q)) //. move: (dvdr_trans Hpp pp1)=> H'. case/andP: (ppC a0)=> H1 _. by move: (dvdr_trans H' (dvdr_mul H1 (dvdrr (pp q)))); rewrite mul1r. rewrite (dvdr_trans _ Hg3) /=; last by move: (dvdr_mul H pq2); rewrite mulr1. case/andP: (pp_prim pq)=> G1 _. by rewrite (dvdr_trans (dvdr_trans Hpp G1)); case/andP: (pp_mull q a0). 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)