let i2, i1 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 INT_1:def 6;
then (i1 / i2) * i2 <= (i1 div i2) * i2 by A2, XREAL_1:65;
then i1 <= (i1 div i2) * i2 by A2, XCMPLX_1:87;
then i1 - ((i1 div i2) * i2) <= 0 by XREAL_1:47;
hence i1 mod i2 <= 0 by INT_1:def 10; :: thesis: verum

end;

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

hence i1 mod i2 <= 0 by INT_1:def 10; :: thesis: verum

end;

end;