theorem Th16: :: NUMBER03:16
for a, b, n being Nat st a < n & b < n & n divides a - b holds
a = b