diff --git a/Lebesgue/bochner_integral/BInt_Bif.v b/Lebesgue/bochner_integral/BInt_Bif.v
index a787980c5ed1d8b0dd0571ead8a6bd6dd4fb1044..20b87536765cfcf0c0d63e77ee5eb73e679d22e8 100644
--- a/Lebesgue/bochner_integral/BInt_Bif.v
+++ b/Lebesgue/bochner_integral/BInt_Bif.v
@@ -29,6 +29,16 @@ From Coquelicot Require Import
     Lim_seq
 .
 
+From Lebesgue Require Import
+    measure
+    LInt_p
+    Rbar_compl
+    simple_fun
+    measurable_fun
+    sigma_algebra
+    sigma_algebra_R_Rbar
+.
+
 Require Import
     hierarchy_notations
     simpl_fun
@@ -39,16 +49,6 @@ Require Import
     series
 .
 
-Require Import
-    measure
-    LInt_p
-    Rbar_compl
-    simple_fun
-    measurable_fun
-    sigma_algebra
-    sigma_algebra_R_Rbar
-.
-
 
 Section BInt_def.
 
diff --git a/Lebesgue/bochner_integral/BInt_LInt_p.v b/Lebesgue/bochner_integral/BInt_LInt_p.v
index 15e3f279dfbf4aa848c51aa51dc892b3f49c7683..48c9d1054dfb902ea221d39d6c70a01182f82f14 100644
--- a/Lebesgue/bochner_integral/BInt_LInt_p.v
+++ b/Lebesgue/bochner_integral/BInt_LInt_p.v
@@ -32,6 +32,17 @@ From Coquelicot Require Import
     Lim_seq
 .
 
+From Lebesgue Require Import
+    Rbar_compl
+    Subset_charac
+    sigma_algebra
+    sigma_algebra_R_Rbar
+    measurable_fun
+    measure
+    simple_fun
+    LInt_p
+.
+
 Require Import
     hierarchy_notations
     simpl_fun
@@ -44,17 +55,6 @@ Require Import
     BInt_Bif
 .
 
-Require Import
-    Rbar_compl
-    Subset_charac
-    sigma_algebra
-    sigma_algebra_R_Rbar
-    measurable_fun
-    measure
-    simple_fun
-    LInt_p
-.
-
 
 Section BInt_to_LInt_p.
 
diff --git a/Lebesgue/bochner_integral/BInt_R.v b/Lebesgue/bochner_integral/BInt_R.v
index e38f63b1a73b03a97daf0c28be5c6cb312b71223..e84d2832323c9a2ad92871c526357193b07dd833 100644
--- a/Lebesgue/bochner_integral/BInt_R.v
+++ b/Lebesgue/bochner_integral/BInt_R.v
@@ -31,6 +31,16 @@ From Coquelicot Require Import
     Lim_seq
 .
 
+From Lebesgue Require Import
+    measure
+    LInt_p
+    Rbar_compl
+    simple_fun
+    measurable_fun
+    sigma_algebra
+    sigma_algebra_R_Rbar
+.
+
 Require Import
     hierarchy_notations
     simpl_fun
@@ -41,16 +51,6 @@ Require Import
     series
     Bi_fun
     BInt_Bif
-.
-
-Require Import
-    measure
-    LInt_p
-    Rbar_compl
-    simple_fun
-    measurable_fun
-    sigma_algebra
-    sigma_algebra_R_Rbar
     BInt_LInt_p
 .
 
diff --git a/Lebesgue/bochner_integral/B_spaces.v b/Lebesgue/bochner_integral/B_spaces.v
index fb45ce47afcd06c5df028c6a044bdd5b81b6a780..76fe97caa506abcb612d2e9d5e312e480798d695 100644
--- a/Lebesgue/bochner_integral/B_spaces.v
+++ b/Lebesgue/bochner_integral/B_spaces.v
@@ -33,6 +33,16 @@ From Coquelicot Require Import
     Lim_seq
 .
 
+From Lebesgue Require Import
+    measure
+    LInt_p
+    Rbar_compl
+    simple_fun
+    measurable_fun
+    sigma_algebra
+    sigma_algebra_R_Rbar
+.
+
 Require Import
     hierarchy_notations
     simpl_fun
@@ -47,16 +57,6 @@ Require Import
     BInt_LInt_p
 .
 
-Require Import
-    measure
-    LInt_p
-    Rbar_compl
-    simple_fun
-    measurable_fun
-    sigma_algebra
-    sigma_algebra_R_Rbar
-.
-
 
 Section ae_eq_prop.
 
diff --git a/Lebesgue/bochner_integral/Bi_fun.v b/Lebesgue/bochner_integral/Bi_fun.v
index fd8998f0698dc3aaae122793ebc22f61f2c49d9b..9531ae05ceb57af3ff26de03a596b795fd6d3e83 100644
--- a/Lebesgue/bochner_integral/Bi_fun.v
+++ b/Lebesgue/bochner_integral/Bi_fun.v
@@ -32,16 +32,6 @@ From Coquelicot Require Import
     Markov
 .
 
-Require Import
-    hierarchy_notations
-    simpl_fun
-    BInt_sf
-    Bsf_Lsf
-    CUS_Lim_seq
-    topology_compl
-    series
-.
-
 From Lebesgue Require Import
     measure
     LInt_p
@@ -55,6 +45,16 @@ From Lebesgue Require Import
     logic_compl
 .
 
+Require Import
+    hierarchy_notations
+    simpl_fun
+    BInt_sf
+    Bsf_Lsf
+    CUS_Lim_seq
+    topology_compl
+    series
+.
+
 
 Lemma is_LimSup_seq_Rbar_scal_l :
   forall u : nat -> Rbar, forall a : R, 0%R <= a -> forall l : R, is_LimSup_seq_Rbar u l ->
diff --git a/Lebesgue/bochner_integral/complete_normed_module_series.v b/Lebesgue/bochner_integral/complete_normed_module_series.v
index 78bcc15cc0a351a5de0d777dc1d443b0b41d8891..94297dcefcadb529c971374d53596651221544ca 100644
--- a/Lebesgue/bochner_integral/complete_normed_module_series.v
+++ b/Lebesgue/bochner_integral/complete_normed_module_series.v
@@ -21,6 +21,7 @@ From Coq Require Import
     Rbasic_fun
     RIneq
 .
+
 From Coquelicot Require Import
     Hierarchy
     Series
diff --git a/Lebesgue/bochner_integral/topology_compl.v b/Lebesgue/bochner_integral/topology_compl.v
index 28ef73a634457d4d4584a4afe3a95f32ed751710..37d3ed15977d764c8e25162c69f46b3696423e9b 100644
--- a/Lebesgue/bochner_integral/topology_compl.v
+++ b/Lebesgue/bochner_integral/topology_compl.v
@@ -30,12 +30,15 @@ From Coquelicot Require Import
     Lub
 .
 
-Require Import
+From Lebesgue Require Import
     countable_sets
-    hierarchy_notations
     Rbar_compl
 .
 
+Require Import
+    hierarchy_notations
+.
+
 
 Section open_subspaces.