theorem :: WSIERP_1:42

for k being Integer
for n being Nat st k mod n = 0 holds
- (k div n) = (- k) div n