theorem ND1: :: NEWTON07:1

for k, n being non zero Nat st k mod n = 0 holds
(k - 1) mod n = n - 1