for k, n being Nat st k <> 0 holds
(n + k) div k = (n div k) + 1