theorem Th1: :: NTALGO_1:1

for x, p being Integer holds (x mod p) mod p = x mod p by NAT_D:73;