proposition: Lemma pp_mul : forall p q, pp (p * q) %= pp p * pp q.
proof: Proof. move=> p q. have [-> | p0] := eqVneq p 0; first by rewrite mul0r !pp0 mul0r. have [-> | q0] := eqVneq q 0; first by rewrite mulr0 !pp0 mulr0. have h0: (gcdsr (p * q))%:P != 0. by rewrite polyC_eq0 gcdsr_eq0 mulf_eq0 negb_or p0. have h1: pp p * pp q != 0. by rewrite mulf_eq0 !pp_eq0 negb_or p0. rewrite -(@eqd_mul2l (poly_of R) (gcdsr (p * q))%:P)// -ppP. move: (polyC_inj_eqd (gauss_lemma p q)). rewrite -(eqd_mul2r _ _ h1)=> H; rewrite eqd_sym (eqd_trans H) //. by rewrite polyCM mulrCA -mulrA -ppP mulrCA mulrA -ppP. 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)