theorem Th2: :: PELLS_EQ:2

for i, j being Integer st j <> 0 holds
|.(i mod j).| < |.j.|