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:74;
then i / j < 0 + 1 by A1, XCMPLX_1:60;
then (i / j) - 1 < 0 by XREAL_1:19;
then [\(i / j)/] = 0 by A1, INT_1:def 6;
hence i div j = 0 by INT_1:def 9; :: thesis: verum