proposition: Fact 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); [left|right]. - apply mod_pos_bound; trivial. - apply mod_neg_bound; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv