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