diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v
index 3d5d709155be528f93bbd411159aae697cee7d74..0aab3c081c03e86a93191d2c6d9cd30eb466b20a 100644
--- a/Lebesgue/measurable_Rbar.v
+++ b/Lebesgue/measurable_Rbar.v
@@ -532,14 +532,19 @@ Proof.
 rewrite measurable_Rbar_eq_Borel, measurable_Rbar_R_alt_correct; easy.
 Qed.
 
+(* WIP [lazy]: wait for actually needing it...
 Lemma measurable_Rbar_abs :
   forall B, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_abs y)).
 Proof.
 Admitted.
+*)
 
+(* WIP [lazy]: wait for actually needin it...
 Lemma measurable_Rbar_scal :
-  forall B l, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
+  forall B l,
+    measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
 Proof.
 Admitted.
+*)
 
 End measurable_Rbar.