proposition: Lemma div_opp_opp : forall a b, b~=0 -> -a/-b == a/b.
proof: Proof. intros a b **. symmetry. apply div_unique with (- (a mod b)). - now apply opp_mod_bound_or. - rewrite mul_opp_l, <- opp_add_distr, <- div_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv