proposition: Lemma Cint_rat a : (QtoC a \in Num.int) = (a \in Num.int).
proof: Proof. apply/idP/idP=> [Za | /numqK <-]; last by rewrite rmorph_int. apply/intrP; exists (Num.floor (QtoC a)); apply: (can_inj ratCK). by rewrite rmorph_int floorK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)