theorem :: INT_1:56

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