theorem Th80: :: NEWTON02:80

for a, n, k being Nat holds (k * ((a * n) + 1)) mod a = k mod a