proposition: Lemma div_opp_r : forall a b, b~=0 -> a/(-b) == -(a/b).
proof: Proof. intros. symmetry. apply div_unique with (a mod b). - rewrite abs_opp; now apply mod_always_pos. - rewrite mul_opp_opp; now apply div_mod. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv