theorem :: INT_1:57

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