lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;