proposition: Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b).
proof: Proof. intros a b ?. assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0). rewrite <- (mul_cancel_l _ _ (-b)) by trivial. rewrite <- (add_cancel_r _ _ (a rem (-b))). now rewrite <- quot_rem, rem_opp_r, mul_opp_opp, <- quot_rem. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv