for t, u, z being Integer holds (t + (u mod z)) mod z = (t + u) mod z