The _rev lemmas cannot mention anything about the to_real values. Indeed,
with a directed rounding, in case of overflow, the result might still be
finite, yet be unrelated to the infinitely-precise value.

Note that the lemmas were true for rounding to nearest though (since the
result is necessarily infinite in case of overflow then), so it might be
worth adding back some specialized versions for rounding to nearest.

Note also that lemmas for neg, abs, and sqrt, do not need fixing, since
these operations cannot overflow.

This commit also fixes some issues about to_int_monotonic_int. Indeed,
large integers are not always representable, so we get to_int RNU x = x >
i for x = of_int RNU i.