theorem Th90: :: NEWTON02:90

for t being Integer
for k being positive Nat holds
( t mod k = k - 1 iff (t + 1) mod k = 0 )