(* *)
(**************************************************************************)
-include "lebesgue.ma".
-include "models/nat_order_continuous.ma".
+include "dama/lebesgue.ma".
+include "dama/models/nat_order_continuous.ma".
+alias symbol "dependent_pair" = "dependent pair".
theorem nat_lebesgue_oc:
∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s.
∀x:ℕ.a order_converges x →