proposition: Lemma mod_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 -> (-a) mod b == b - a mod b.
proof: Proof. intros a b Hb H. symmetry. apply mod_unique with (-(a/b)-1). - destruct (lt_ge_cases 0 b); [left|right]. + rewrite le_0_sub. rewrite <- (sub_0_r b) at 5. rewrite <- sub_lt_mono_l. destruct (mod_pos_bound a b); intuition; order. + rewrite le_sub_0. rewrite <- (sub_0_r b) at 1. rewrite <- sub_lt_mono_l. destruct (mod_neg_bound a b); intuition; order. - rewrite <- (add_opp_r b), mul_sub_distr_l, mul_1_r, sub_add_simpl_r_l. rewrite mul_opp_r, <-opp_add_distr, <-div_mod; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv