proposition: Lemma div_str_pos_iff : forall a b, 0<=a -> 0<b -> (0<a/b <-> b<=a).
proof: Proof. intros a b Ha Hb; split; intros Hab. - destruct (lt_ge_cases a b) as [LT|LE]; auto. rewrite <- div_small_iff in LT; order. - apply div_str_pos; auto. Qed.
imports: NZAxioms NZMulOrder