let i, j be Integer; :: thesis: ( j > 0 & i div j = 0 implies i < j )
assume A1: ( j > 0 & i div j = 0 ) ; :: thesis: i < j
then [\(i / j)/] = 0 by INT_1:def 7;
then (i / j) - 1 < 0 by INT_1:def 4;
then i / j < 0 + 1 by XREAL_1:21;
then ( (i / j) * j < 1 * j & j <> 0 ) by A1, XREAL_1:70;
hence i < j by XCMPLX_1:88; :: thesis: verum