proposition: Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
proof: Proof. by apply: size_map_inj_poly; first apply: intr_inj. 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)