proposition: Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b).
proof: Proof. intros a b ?. rewrite <- (mul_cancel_l _ _ b) by trivial. rewrite <- (add_cancel_r _ _ ((-a) rem b)). now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv