proposition: Lemma mod_opp_l_z : forall a b, b~=0 -> a mod b == 0 -> (-a) mod b == 0.
proof: Proof. intros a b Hb Hab. symmetry. apply mod_unique with (-(a/b)). - split; [order|now rewrite abs_pos]. - now rewrite <-opp_0, <-Hab, mul_opp_r, <-opp_add_distr, <-div_mod. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv