let a, b be Integer; :: thesis: for c being non zero Nat holds
( ( (a + b) mod c = b mod c implies a mod c = 0 ) & ( (a + b) mod c <> b mod c implies a mod c > 0 ) )
let c be non zero Nat; :: thesis: ( ( (a + b) mod c = b mod c implies a mod c = 0 ) & ( (a + b) mod c <> b mod c implies a mod c > 0 ) )
L1: ( (a + b) mod c = b mod c implies a mod c = 0 )

proof

assume (a + b) mod c = b mod c ; :: thesis: a mod c = 0
then 0 = (((a + b) mod c) - (b mod c)) mod c
.= ((a + b) - b) mod c by INT_6:7 ;
hence a mod c = 0 ; :: thesis: verum

end;

(a + b) mod c = ((a mod c) + (b mod c)) mod c by NAT_D:66;
then ( a mod c = 0 implies (a + b) mod c = b mod c ) ;
hence ( ( (a + b) mod c = b mod c implies a mod c = 0 ) & ( (a + b) mod c <> b mod c implies a mod c > 0 ) ) by L1, INT_1:57; :: thesis: verum