fact: Definition Z2int (z : BinNums.Z) := match z with | Z0 => 0%:Z | Z.pos p => (nat_of_pos p)%:Z | Z.neg n => (- (nat_of_pos n)%:Z)%R end.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)