theorem :: INT_1:58

for i1, i2 being Integer st i2 > 0 holds
i1 mod i2 < i2