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 that
A2: 0 <= a and
A3: a < n ; :: thesis: a mod n = a
reconsider aa = a as Element of NAT by A2, INT_1:3;
reconsider nn = n as Element of NAT by A2, A3, INT_1:3;
consider t being Nat such that
A4: aa = (nn * t) + (aa mod nn) and
aa mod nn < nn by A1, Def2;
t = 0

proof

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

end;

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

end;

assume that
A6: 0 > a and
A7: a >= - n ; :: thesis: a mod n = n + a
A8: n >= 0 by A6, A7;
A9: (a / n) - 1 < - 1

proof

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

end;

a * (n ") >= (- n) * (n ") by A7, A8, XREAL_1:64;
then a / n >= - (n * (n ")) by XCMPLX_0:def 9;
then - 1 <= a / n by A1, XCMPLX_0:def 7;
then [\(a / n)/] = - 1 by A9, INT_1:def 6;
then A10: a div n = - 1 by INT_1:def 9;
a mod n = a - ((a div n) * n) by A1, INT_1:def 10;
hence a mod n = n + a by A10; :: thesis: verum

end;

end;