proposition: Lemma Cint_rat_Aint z : z \in Crat -> z \in Aint -> z \in Num.int.
proof: Proof. case/CratP=> a ->{z} /polyOverP/(_ 0). have [p [Dp mon_p] dv_p] := minCpolyP (ratr a); rewrite Dp coef_map. suffices /eqP->: p == 'X - a%:P by rewrite polyseqXsubC /= rmorphN rpredN. rewrite -eqp_monic ?monicXsubC // irredp_XsubC //. by rewrite -(size_map_poly QtoC) -Dp neq_ltn size_minCpoly orbT. by rewrite -dv_p fmorph_root root_XsubC. 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)