proposition: Lemma div_small_iff : forall a b, 0<=a -> 0<b -> (a/b==0 <-> a<b).
proof: Proof. intros a b Ha Hb; split; intros Hab. - destruct (lt_ge_cases a b); auto. symmetry in Hab. contradict Hab. apply lt_neq, div_str_pos; auto. - apply div_small; auto. Qed.
imports: NZAxioms NZMulOrder