theorem :: PRE_FF:3

for i, j being Integer st j > 0 & i div j = 0 holds
i < j