let p, n, s be natural Number ; :: thesis: (p + s) mod n = ((p mod n) + s) mod n

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

suppose n > 0 ; :: thesis: (p + s) mod n = ((p mod n) + s) mod n

then (p + s) mod n = (((n * (p div n)) + (p mod n)) + s) mod n by INT_1:59
.= ((n * (p div n)) + ((p mod n) + s)) mod n
.= ((p mod n) + s) mod n by Th21 ;
hence (p + s) mod n = ((p mod n) + s) mod n ; :: thesis: verum

end;

suppose A1: n = 0 ; :: thesis: (p + s) mod n = ((p mod n) + s) mod n

hence (p + s) mod n = 0 by Def2
.= ((p mod n) + s) mod n by A1, Def2 ;
:: thesis: verum

end;

end;