Order (imports) + renaming (section).

Lebesgue/measurable_R.v

@@ -17,9 +17,10 @@ COPYING file for more details.
 From Coq Require Import Qreals Reals Lra.
 From Coquelicot Require Import Hierarchy.
 
-Require Import countable_sets topo_bases_R R_compl.
+Require Import R_compl countable_sets topo_bases_R.
 Require Import Subset Subset_dec Subset_seq Subset_R.
-Require Import Subset_system_base Subset_system measurable.
+Require Import Subset_system_base Subset_system.
+Require Import measurable.
 
 Open Scope R_scope.
 
@@ -41,7 +42,7 @@ Inductive gen_R_Qoo : (R -> Prop) -> Prop :=
 End gen_R_Def.
 
 
-Section gen_R_eq.
+Section measurable_R_Borel_eq.
 
 Lemma measurable_R_Borel_singleton : forall (x : R), measurable_Borel (singleton x).
 Proof.
@@ -214,7 +215,7 @@ apply measurable_Borel_closed, closed_le.
 apply measurable_R_Borel_eq_oc.
 Qed.
 
-End gen_R_eq.
+End measurable_R_Borel_eq.
 
 
 Section measurable_R.