theorem :: WSIERP_1:41

for k being Integer
for n being Nat st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1