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 Hab. symmetry. apply div_unique with (-(a mod b)). - rewrite Hab, opp_0. split; [order|]. pos_or_neg b; [rewrite abs_eq | rewrite abs_neq']; order. - now rewrite mul_opp_r, <-opp_add_distr, <-div_mod. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv