proposition: Lemma mod_opp_r_nz : forall a b, b~=0 -> a mod b ~= 0 -> a mod (-b) == (a mod b) - b.
proof: Proof. intros a b **. rewrite <- (opp_involutive a) at 1. rewrite mod_opp_opp, mod_opp_l_nz by trivial. now rewrite opp_sub_distr, add_comm, add_opp_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv