for k, n being Nat holds
( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )