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