proposition: Lemma root_monic_Aint p x : root p x -> p \is monic -> p \is a polyOver Num.int -> x \in Aint.
proof: Proof. have pZtoQtoC pz: pQtoC (pZtoQ pz) = pZtoC pz. by rewrite -map_poly_comp; apply: eq_map_poly => b; rewrite /= rmorph_int. move=> px0 mon_p /floorpP[pz Dp]; rewrite unfold_in. move: px0; rewrite Dp -pZtoQtoC; have [q [-> mon_q] ->] := minCpolyP x. case/dvdpP_rat_int=> qz [a nz_a Dq] [r]. move/(congr1 (fun q1 => lead_coef (a *: pZtoQ q1))). rewrite rmorphM scalerAl -Dq lead_coefZ lead_coefM /=. have /monicP->: pZtoQ pz \is monic by rewrite -(map_monic QtoC) pZtoQtoC -Dp. rewrite (monicP mon_q) mul1r mulr1 lead_coef_map_inj //; last exact: intr_inj. rewrite Dq => ->; apply/polyOverP=> i; rewrite !(coefZ, coef_map). by rewrite -rmorphM /= rmorph_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)