proposition: Lemma ppP : forall p, p = (gcdsr p)%:P * pp p.
proof: Proof. move=> p. have [-> | p0] := eqVneq p 0; first by rewrite pp0 mulr0. have g0 : (gcdsr p)%:P != 0 by rewrite polyC_eq0 gcdsr_eq0. case: (gcdsr_odivp p0) => x [hx px]. by rewrite /pp hx; move: (odivr_some hx)=> {1}->. 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)