proposition: Fact opp_mod_bound_or : forall a b, b~=0 -> 0 <= -(a mod b) < -b \/ -b < -(a mod b) <= 0.
proof: Proof. intros a b **. destruct (lt_ge_cases 0 b); [right|left]. - rewrite <- opp_lt_mono, opp_nonpos_nonneg. destruct (mod_pos_bound a b); intuition; order. - rewrite <- opp_lt_mono, opp_nonneg_nonpos. destruct (mod_neg_bound a b); intuition; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv