let a, b, c, n be Integer; :: thesis: ((a + b) + c) mod n = (((a mod n) + (b mod n)) + (c mod n)) mod n
thus ((a + b) + c) mod n = (((a + b) mod n) + (c mod n)) mod n by NAT_D:66
.= ((((a mod n) + (b mod n)) mod n) + ((c mod n) mod n)) mod n by NAT_D:66
.= (((a mod n) + (b mod n)) + (c mod n)) mod n by NAT_D:66 ; :: thesis: verum