let i1, i2 be Integer; :: thesis: ( i2 > 0 implies i1 mod i2 < i2 )
assume A1: i2 > 0 ; :: thesis: i1 mod i2 < i2
(i1 / i2) - 1 < [\(i1 / i2)/] by Def6;
then ((i1 / i2) - 1) * i2 < (i1 div i2) * i2 by A1, XREAL_1:68;
then ((i1 / i2) * i2) - (1 * i2) < (i1 div i2) * i2 ;
then i1 - i2 < ((i1 div i2) * i2) - 0 by A1, XCMPLX_1:87;
then i1 - ((i1 div i2) * i2) < i2 - 0 by XREAL_1:17;
hence i1 mod i2 < i2 by A1, Def10; :: thesis: verum