theorem :: PRE_FF:4

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