fact: Definition rat2bigQ (q : rat) : bigQ := let n := BigZ.of_Z (int2Z (numq q)) in let d := BigN.N_of_Z (int2Z (denq q)) in (n # d)%bigQ.
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)