let i2, i1 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 INT_1:def 6;
then (i1 div i2) * i2 < ((i1 / i2) - 1) * i2 by A1, XREAL_1:69;
then (i1 div i2) * i2 < ((i1 / i2) * i2) - (1 * i2) ;
then (i1 div i2) * i2 < i1 - i2 by A1, XCMPLX_1:87;
then ((i1 div i2) * i2) - i1 < (i1 - i2) - i1 by XREAL_1:14;
then - (i1 - ((i1 div i2) * i2)) < - i2 ;
hence - (i1 mod i2) < - i2 by A1, INT_1:def 10; :: thesis: verum