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 H. symmetry. apply mod_unique with (-(a/b)). - destruct (lt_ge_cases 0 b); [left|right]; intuition auto; order. - rewrite <- opp_0, <- H. rewrite mul_opp_r, <- opp_add_distr, <- div_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv