More compact.

Lebesgue/Subset_R.v

@@ -576,14 +576,14 @@ rewrite HP; clear HP; unfold a, b, get_useful; clear a b.
 apply subset_ext_equiv; split.
 (* . *)
 intros x [p [Hx1 [Hx2 Hx3]]].
-case optN as [N | ]; destruct HB as [HB1 HB2]; destruct (HB2 p Hx1) as [n Hn].
+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.
-case optN as [N | ]; destruct HB as [HB1 HB2].
+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.
 Qed.