for x, y being Integer st |.y.| <> 0 holds
|.(x mod y).| < |.y.|