theorem :: NAT_D:73

for m, n being Integer holds (m mod n) mod n = m mod n