proposition: Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> 0<=a<b \/ b<a<=0).
proof: Proof. intros a b Hb. split. - intros EQ. rewrite (div_mod a b Hb), EQ; nzsimpl. now apply mod_bound_or. - destruct 1. + now apply div_small. + rewrite <- div_opp_opp by trivial. apply div_small; trivial. rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv