Mv Import.

Lebesgue/Subset_R.v

@@ -17,7 +17,7 @@ COPYING file for more details.
 From Coq Require Import Lia Reals Lra.
 From Coquelicot Require Import Coquelicot.
 
-Require Import R_compl Rbar_compl.
+Require Import R_compl Rbar_compl countable_sets topo_bases_R.
 Require Import Subset Subset_dec Subset_seq.
 Require Import Subset_system_base.
 
@@ -532,9 +532,6 @@ Definition R_subset_open : (R -> Prop) -> Prop :=
 End R_subset_open_Def.
 
 
-Require Import nat_compl countable_sets topo_bases_R.
-
-
 Section R_subset_open_Facts.
 
 (** Correctness results. *)