theorem Th1: :: NAT_D:1

for i, j being natural Number st 0 < i holds
j mod i < i by INT_1:58;