diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v
index 0c17a5de292a03d623711a78f49dbdfb08caa039..c1ee157cf3a4cbe7cb731cdd3cb41a47b47d9795 100644
--- a/Lebesgue/measurable_Rbar.v
+++ b/Lebesgue/measurable_Rbar.v
@@ -500,9 +500,9 @@ Proof.
 rewrite measurable_Rbar_eq_Borel; apply measurable_Rbar_Borel_singleton.
 Qed.
 
-Lemma measurable_Rbar_eq_le : measurable_Rbar = measurable gen_Rbar_le.
+Lemma measurable_Rbar_eq_ge : measurable_Rbar = measurable gen_Rbar_ge.
 Proof.
-rewrite <- measurable_Rbar_Borel_eq_le, measurable_Rbar_Borel_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_ge, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
 Lemma measurable_Rbar_eq_gt : measurable_Rbar = measurable gen_Rbar_gt.
@@ -510,84 +510,56 @@ Proof.
 rewrite <- measurable_Rbar_Borel_eq_gt, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
-Lemma measurable_Rbar_eq_ge : measurable_Rbar = measurable gen_Rbar_ge.
+Lemma measurable_Rbar_eq_le : measurable_Rbar = measurable gen_Rbar_le.
 Proof.
-rewrite <- measurable_Rbar_Borel_eq_ge, measurable_Rbar_Borel_eq_lt; easy.
+rewrite <- measurable_Rbar_Borel_eq_le, measurable_Rbar_Borel_eq_lt; easy.
 Qed.
 
-Lemma measurable_Rbar_lt_R : forall (a : R), measurable_Rbar (Rbar_lt a).
+Lemma measurable_Rbar_ge : forall b, measurable_Rbar (Rbar_ge b).
 Proof.
-intros; apply measurable_gen; easy.
+intros; apply measurable_Rbar_closed, closed_Rbar_ge.
 Qed.
 
-Lemma measurable_Rbar_lt : forall a, measurable_Rbar (Rbar_lt a).
-Proof.
-intros a; destruct a.
-apply measurable_Rbar_lt_R.
-apply measurable_ext with emptyset; try easy; apply measurable_empty.
-apply measurable_ext with (union_seq (fun n => Rbar_lt (- INR n))).
-admit.
-apply measurable_union_seq; intros n; apply measurable_Rbar_lt_R.
-Admitted.
-
-Lemma measurable_Rbar_le_R : forall (a : R), measurable_Rbar (Rbar_le a).
+Lemma measurable_Rbar_gt : forall b, measurable_Rbar (Rbar_gt b).
 Proof.
-intros; rewrite measurable_Rbar_eq_le; apply measurable_gen; easy.
+intros; apply measurable_Rbar_open, open_Rbar_gt.
 Qed.
 
 Lemma measurable_Rbar_le : forall a, measurable_Rbar (Rbar_le a).
 Proof.
-intros a; destruct a.
-apply measurable_Rbar_le_R.
-apply measurable_ext with (singleton p_infty).
-Rbar_interval_full_unfold; intros y; destruct y; easy.
-apply measurable_Rbar_singleton.
-apply measurable_ext with fullset; try easy.
-apply measurable_full.
+intros; apply measurable_Rbar_closed, closed_Rbar_le.
 Qed.
 
-Lemma measurable_Rbar_gt : forall b, measurable_Rbar (Rbar_gt b).
+Lemma measurable_Rbar_lt : forall a, measurable_Rbar (Rbar_lt a).
 Proof.
-intros; apply measurable_compl_rev.
-
-(* We need Rbar_le_not_gt. *)
-
-Admitted.
+intros; apply measurable_Rbar_open, open_Rbar_lt.
+Qed.
 
-Lemma measurable_Rbar_ge : forall b, measurable_Rbar (Rbar_ge b).
+Lemma measurable_Rbar_cc : forall a b, measurable_Rbar (Rbar_cc a b).
 Proof.
-intros; apply measurable_compl_rev.
-
-(* We need Rbar_lt_not_ge. *)
-
-Admitted.
+intros; apply measurable_Rbar_closed, closed_Rbar_intcc.
+Qed.
 
-Lemma measurable_Rbar_oo : forall a b, measurable_Rbar (Rbar_oo a b).
+Lemma measurable_Rbar_co : forall a b, measurable_Rbar (Rbar_co a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_lt.
-apply measurable_Rbar_gt.
+intros; apply measurable_inter;
+    [apply measurable_Rbar_le | apply measurable_Rbar_gt].
 Qed.
 
 Lemma measurable_Rbar_oc : forall a b, measurable_Rbar (Rbar_oc a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_lt.
-apply measurable_Rbar_ge.
+intros; apply measurable_inter;
+    [apply measurable_Rbar_lt | apply measurable_Rbar_ge].
 Qed.
 
-Lemma measurable_Rbar_co : forall a b, measurable_Rbar (Rbar_co a b).
+Lemma measurable_Rbar_oo : forall a b, measurable_Rbar (Rbar_oo a b).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_le.
-apply measurable_Rbar_gt.
+intros; apply measurable_Rbar_open, open_Rbar_intoo.
 Qed.
 
-Lemma measurable_Rbar_cc : forall a b, measurable_Rbar (Rbar_cc a b).
+Lemma measurable_Rbar_scal :
+  forall B l, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
 Proof.
-intros; apply measurable_inter.
-apply measurable_Rbar_le.
-apply measurable_Rbar_ge.
-Qed.
+Admitted.
 
 End measurable_Rbar.