theorem ND4: :: NEWTON07:4

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