for rh0 being Element of REAL
for p, q being Integer st p,q are_coprime holds
ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2