proposition: Lemma mod_opp_r_z : forall a b, b~=0 -> a mod b == 0 -> a mod (-b) == 0.
proof: Proof. intros a b **. rewrite <- (opp_involutive a) at 1. now rewrite mod_opp_opp, mod_opp_l_z, opp_0. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv