proposition: Lemma div_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 -> (-a)/b == -(a/b)-sgn b.
proof: Proof. intros a b Hb Hab. symmetry. apply div_unique with (abs b -(a mod b)). - rewrite lt_sub_lt_add_l. rewrite <- le_add_le_sub_l. nzsimpl. rewrite <- (add_0_l (abs b)) at 2. rewrite <- add_lt_mono_r. destruct (mod_always_pos a b); intuition order. - rewrite <- 2 add_opp_r, mul_add_distr_l, 2 mul_opp_r. rewrite sgn_abs. rewrite add_shuffle2, add_opp_diag_l; nzsimpl. rewrite <-opp_add_distr, <-div_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv