let n, a, b be Integer; :: thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n

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

suppose A1: n = 0 ; :: thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n

hence (a - b) mod n = 0 by INT_1:def 10
.= ((a mod n) - (b mod n)) mod n by A1, INT_1:def 10 ;
:: thesis: verum

end;

suppose A2: n <> 0 ; :: thesis: (a - b) mod n = ((a mod n) - (b mod n)) mod n

then A3: (b mod n) + ((b div n) * n) = (b - ((b div n) * n)) + ((b div n) * n) by INT_1:def 10;
(a mod n) + ((a div n) * n) = (a - ((a div n) * n)) + ((a div n) * n) by A2, INT_1:def 10;
then (a - b) - ((a mod n) - (b mod n)) = ((a div n) - (b div n)) * n by A3;
then n divides (a - b) - ((a mod n) - (b mod n)) by INT_1:def 3;
hence (a - b) mod n = ((a mod n) - (b mod n)) mod n by NAT_D:64, INT_2:15; :: thesis: verum

end;

end;