WIP: lazy mode.

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.