theorem Th4: :: NUMPOLY1:4

for n, k being Nat st k <> 0 holds
n,n mod k are_congruent_mod k