proposition: Lemma dvdpP_rat_int p q : p %| pZtoQ q -> {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 * r}}.
proof: Proof. have{p} [p [a nz_a ->]] := rat_poly_scale p. rewrite dvdpZl ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q. exists (zprimitive p); last exact: dvdpP_int. have [-> | nz_p] := eqVneq p 0. by exists 1; rewrite ?oner_eq0 // zprimitive0 map_poly0 !scaler0. exists ((zcontents p)%:~R / a%:~R). by rewrite mulf_neq0 ?invr_eq0 ?intr_eq0 ?zcontents_eq0. by rewrite mulrC -scalerA -map_polyZ -zpolyEprim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)