theorem Th2: :: IDEA_1:2

for n, k1, k2 being Nat st n <> 0 & k1 mod n = k2 mod n & k1 <= k2 holds
ex t being Nat st k2 - k1 = n * t