proposition: Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b).
proof: Proof. intros a b ?. pos_or_neg a; pos_or_neg b. - rewrite NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order. - rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.div_small_iff by order. rewrite (abs_eq a), (abs_neq' b); intuition; order. - rewrite <- opp_inj_wd, opp_0, <- quot_opp_l, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_eq b); intuition; order. - rewrite <- quot_opp_opp, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_neq' b); intuition; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv