theorem :: NAT_2:15

for i, k, n being Nat st k divides n & 1 <= n & 1 <= i & i <= k holds
(n -' i) div k = (n div k) - 1