theorem ND3: :: NEWTON07:3

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