proposition: Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).
proof: Proof. apply/dvdpP/Pdiv.Idomain.dvdpP=> [[/= r1 Dq] | [[/= a r] nz_a Dq]]; last first. exists (a%:~R^-1 *: pZtoQ r); rewrite -scalerAl -rmorphM -Dq /=. by rewrite -{2}[a]intz scaler_int rmorphMz -scaler_int scalerK ?intr_eq0. have [r [a nz_a Dr1]] := rat_poly_scale r1; exists (a, r) => //=. apply: (map_inj_poly _ _ : injective pZtoQ) => //; first exact: intr_inj. rewrite -[a]intz scaler_int rmorphMz -scaler_int /= Dq Dr1. by rewrite -scalerAl -rmorphM scalerKV ?intr_eq0. 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)