From 60a7a33e3a55dc707fc082d7c401fa7a262f1316 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 21 Mar 2022 19:56:43 +0100
Subject: [PATCH] More compact.
---
Lebesgue/Subset_R.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Lebesgue/Subset_R.v b/Lebesgue/Subset_R.v
index 6c257830..274c34cf 100644
--- a/Lebesgue/Subset_R.v
+++ b/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.
--
GitLab