proposition: Lemma div_opp_r_z : forall a b, b~=0 -> a mod b == 0 -> a/(-b) == -(a/b).
proof: Proof. intros a b **. rewrite <- (opp_involutive a) at 1. rewrite div_opp_opp; auto using div_opp_l_z. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv