proposition: Lemma dvdC_int (p : nat) x : x \in Num.int -> (p %| x)%C = (p %| `|Num.floor x|)%N.
proof: Proof. move=> Zx; rewrite -{1}(floorK Zx) {1}[Num.floor x]intEsign. by rewrite rmorphMsign rpredMsign dvdC_nat. 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)