let n, a be Integer; :: thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )

hence ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) ) ; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: ( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )

hereby :: thesis: ( 0 > a & a >= - n implies a mod n = n + a )

assume A2: ( 0 <= a & a < n ) ; :: thesis: a mod n = a
then reconsider aa = a as Element of NAT by INT_1:16;
reconsider nn = n as Element of NAT by A2, INT_1:16;
consider t being Nat such that
A3: ( aa = (nn * t) + (aa mod nn) & aa mod nn < nn ) by A1, NAT_D:def 2;
t = 0

proof

assume A4: t <> 0 ; :: thesis: contradiction
t >= 1 + 0 by A4, INT_1:20;
then A5: t * n >= 1 * n by A2, XREAL_1:66;
(nn * t) + (aa mod nn) >= nn * t by NAT_1:11;
hence contradiction by A2, A3, A5, XXREAL_0:2; :: thesis: verum

end;

hence a mod n = a by A3; :: thesis: verum

end;

assume A6: ( 0 > a & a >= - n ) ; :: thesis: a mod n = n + a
then A7: n >= 0 ;
A8: a mod n = a - ((a div n) * n) by A1, INT_1:def 8;
A9: - 1 <= a / n

proof

n " > 0 by A1, A7;
then a * (n " ) >= (- n) * (n " ) by A6, XREAL_1:66;
then a / n >= - (n * (n " )) by XCMPLX_0:def 9;
hence - 1 <= a / n by A1, XCMPLX_0:def 7; :: thesis: verum

end;

(a / n) - 1 < - 1

proof

assume (a / n) - 1 >= - 1 ; :: thesis: contradiction
then ((a / n) - 1) + 1 >= (- 1) + 1 by XREAL_1:8;
then a * (n " ) >= 0 by XCMPLX_0:def 9;
then (a * (n " )) * n >= 0 * n by A7;
then a * ((n " ) * n) >= 0 ;
then a * 1 >= 0 by A1, XCMPLX_0:def 7;
hence contradiction by A6; :: thesis: verum

end;

then [\(a / n)/] = - 1 by A9, INT_1:def 4;
then a div n = - 1 by INT_1:def 7;
hence a mod n = n + a by A8; :: thesis: verum

end;

end;