let i1, i2 be Integer; :: thesis: ( i2 >= 0 implies i1 mod i2 >= 0 )
assume A1: i2 >= 0 ; :: thesis: i1 mod i2 >= 0

per cases ( i2 > 0 or i2 = 0 ) by A1;

suppose A2: i2 > 0 ; :: thesis: i1 mod i2 >= 0

[\(i1 / i2)/] <= i1 / i2 by Def6;
then (i1 div i2) * i2 <= (i1 / i2) * i2 by A2, XREAL_1:64;
then (i1 div i2) * i2 <= i1 by A2, XCMPLX_1:87;
then i1 - ((i1 div i2) * i2) >= 0 by XREAL_1:48;
hence i1 mod i2 >= 0 by Def10; :: thesis: verum

end;

suppose i2 = 0 ; :: thesis: i1 mod i2 >= 0

hence i1 mod i2 >= 0 by Def10; :: thesis: verum

end;

end;