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