let i, j be Integer; :: thesis: ( j > 0 & i div j = 0 implies i < j )
assume that
A1: j > 0 and
A2: i div j = 0 ; :: thesis: i < j
[\(i / j)/] = 0 by A2, INT_1:def 9;
then (i / j) - 1 < 0 by INT_1:def 6;
then i / j < 0 + 1 by XREAL_1:19;
then (i / j) * j < 1 * j by A1, XREAL_1:68;
hence i < j by A1, XCMPLX_1:87; :: thesis: verum