Proof without keep_useful/get_useful.

Lebesgue/Subset_R.v

@@ -568,24 +568,24 @@ destruct HA as [a [b HA]]; rewrite HA.
 unfold union_seq; apply open_or_count; intros n; apply open_intoo.
 (* *)
 destruct (R_second_countable_alt A HA) as [P HP].
-destruct (keep_useful P) as [phi [optN HB]].
-pose (a := get_useful (fun n => fst (bij_NQ2 n)) 0 phi optN).
-pose (b := get_useful (fun n => snd (bij_NQ2 n)) 0 phi optN).
-exists a, b.
-rewrite HP; clear HP; unfold a, b, get_useful; clear a b.
-apply subset_ext_equiv; split.
-(* . *)
-intros x [p [Hx1 [Hx2 Hx3]]].
-destruct optN as [N | ], HB as [HB1 HB2], (HB2 p Hx1) as [n Hn].
-destruct Hn as [Hn1 Hn2]; exists n; case (lt_dec n (S N)); intros Hn;
-    try easy; split; rewrite <- Hn2; easy.
-exists n; split; rewrite <- Hn; easy.
-(* . *)
-intros x [n [Hx1 Hx2]].
-exists (phi n); generalize Hx1, Hx2; clear Hx1 Hx2.
-destruct optN as [N | ], HB as [HB1 HB2].
-case (lt_dec n (S N)); intros Hn Hx1 Hx2; try lra; split; try apply HB1; easy.
-intros Hx1 Hx2; split; try apply HB1; easy.
+unfold R_subset_open.
+pose (a := fun n =>
+    match (in_dec P n) with
+    | left _ => fst (bij_NQ2 n)
+    | right _ => 0%Q
+    end).
+pose (b := fun n =>
+    match (in_dec P n) with
+    | left _ => snd (bij_NQ2 n)
+    | right _ => 0%Q
+    end).
+exists a, b; rewrite HP; f_equal.
+apply subset_seq_ext.
+intros n; unfold a, b; destruct (in_dec P n) as [Hn | Hn].
+rewrite (subset_ext (Prop_cst (P n)) fullset); try easy.
+rewrite inter_full_l; easy.
+rewrite (subset_ext (Prop_cst (P n)) emptyset); try easy.
+rewrite inter_empty_l, R_oo_diag_is_empty; easy.
 Qed.
 
 End R_subset_open_Facts.