for a, b, r being Real st r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b holds
a = b