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