proposition: Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> 0<=a<abs b).
proof: Proof. intros a b Hb. split. - intros EQ. rewrite (div_mod a b Hb), EQ; nzsimpl. now apply mod_always_pos. - intros. pos_or_neg b. + apply div_small. now rewrite <- (abs_eq b). + apply opp_inj; rewrite opp_0, <- div_opp_r by trivial. apply div_small. rewrite <- (abs_neq' b) by order. trivial. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv