let x, p be Integer; :: thesis: (x mod p) mod p = x mod p
x mod p = (x + 0) mod p
.= ((x mod p) + (0 mod p)) mod p by NAT_D:66
.= ((x mod p) + 0) mod p by INT_4:12 ;
hence (x mod p) mod p = x mod p ; :: thesis: verum