Add Rbar_oo_diag_is_empty.

Remove useless.

Lebesgue/Subset_Rbar.v

@@ -297,26 +297,6 @@ End Rbar_subset_Facts2.
 
 Section Rbar_subset_Facts3.
 
-Lemma up_m_union_inter_Prop_l :
-  forall A0 A1 P,
-    up_m (union (inter (Prop_cst P) A0) (inter (Prop_cst (~ P)) A1)) =
-    union (inter (Prop_cst P) (up_m A0))
-          (inter (Prop_cst (~ P)) (up_m A1)).
-Proof.
-intros; rewrite up_m_union, 2!up_m_inter.
-Rbar_subset_intros y Hy.
-Qed.
-
-Lemma up_p_union_inter_Prop_l :
-  forall A0 A1 P,
-    up_p (union (inter (Prop_cst P) A0) (inter (Prop_cst (~ P)) A1)) =
-    union (inter (Prop_cst P) (up_p A0))
-          (inter (Prop_cst (~ P)) (up_p A1)).
-Proof.
-intros; rewrite up_p_union, 2!up_p_inter.
-Rbar_subset_intros y Hy.
-Qed.
-
 (** Compatibility of down, lift, and up_* functions
  with countable operations. *)
 
@@ -722,6 +702,13 @@ destruct (Rbar_glb_lt_ex _ _ _ Hm Hy1) as [a [Ha1 [Ha2 Ha3]]],
 apply (HB a b); try apply Rbar_le_trans with y; easy.
 Qed.
 
+Lemma Rbar_oo_diag_is_empty : forall a, Rbar_oo a a = emptyset.
+Proof.
+Rbar_interval_full_unfold; intros a; apply subset_ext_equiv; split; try easy.
+intros y [Hy1 Hy2].
+apply Rbar_lt_not_le in Hy1; apply Rbar_lt_le in Hy2; easy.
+Qed.
+
 End Rbar_interval_Facts.