theorem DIV: :: NEWTON06:21

for a being Integer
for b being non zero Integer st not b divides a holds
(a div b) + ((- a) div b) = - 1