let t, u, z be Integer; :: thesis: (t + (u mod z)) mod z = (t + u) mod z
thus (t + (u mod z)) mod z = (((t mod z) + ((u mod z) mod z)) mod z) mod z by NAT_D:66
.= (t + u) mod z by NAT_D:66 ; :: thesis: verum