for i1, i2 being Integer st i2 >= 0 holds
i1 mod i2 >= 0 by INT_1:57;