proposition: Lemma div_opp_l_z : forall a b, b~=0 -> a mod b == 0 -> (-a)/b == -(a/b).
proof: Proof. intros a b Hb H. symmetry. apply div_unique with 0. - 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