(* *)
(**************************************************************************)
-include "models/increasing_supremum_stabilizes.ma".
-include "models/nat_ordered_uniform.ma".
+include "dama/models/increasing_supremum_stabilizes.ma".
+include "dama/models/nat_ordered_uniform.ma".
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;