theorem Th1: :: RADIX_1:1

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