theorem Th16: :: NUMBER02:16

for a, b, k being Nat st k < a holds
((a * b) + k) mod a = k