let a, b be Integer; :: thesis: a div (- b) = (- a) div b
a div (- b) = (- a) div (- (- b)) by NEWTON06:35;
hence a div (- b) = (- a) div b ; :: thesis: verum