Description taken from the TODO file.
x // y should behave as with any other operation or function, though
the sign convention should match that of x % y: that is, x // y
should be the result of rounding the quotient towards zero.
As with any function that produces a single MPFR result, it's enough
to be able to compute with rounding mode RoundTowardZero and to be
able to detect exactness. It's the second part that's tricky here:
floor(x / y) is exactly n iff n <= x // y < n + 1. Since n may be
something huge, n + 1 shouldn't be computed exactly (since this
might involved billions of bits); instead we need to find an
indirect way of doing this comparison.
Description taken from the TODO file.