theorem Th1: :: PELLS_EQ:1

for i, j being Integer st j < 0 holds
( j < i mod j & i mod j <= 0 )