proposition: Lemma div_opp_opp_nz : forall a b, b~=0 -> a mod b ~= 0 -> (-a)/(-b) == a/b + sgn(b).
proof: Proof. intros. rewrite div_opp_r, div_opp_l_nz by trivial. now rewrite opp_sub_distr, opp_involutive. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv