theorem Th2: :: RADIX_1:2

for k, n being Nat st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1 by NAT_D:70;