proposition: Lemma rat_poly_scale (p : {poly rat}) : {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.
proof: Proof. pose a := \prod_(i < size p) denq p`_i. have nz_a: a != 0 by apply/prodf_neq0=> i _; apply: denq_neq0. exists (map_poly numq (a%:~R *: p)), a => //. apply: canRL (scalerK _) _; rewrite ?intr_eq0 //. apply/polyP=> i; rewrite !(coefZ, coef_map_id0) // numqK // Qint_def mulrC. have [ltip | /(nth_default 0)->] := ltnP i (size p); last by rewrite mul0r. by rewrite [a](bigD1 (Ordinal ltip)) // rmorphM mulrA -numqE -rmorphM denq_int. 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)