From b4dc185d4c5e8180b3afac11afc408d76f20489f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 24 Jun 2025 11:40:35 +0900
Subject: [PATCH 1/2] lemma generalization

Co-authored-by: Alessandro Bruni <brun@itu.dk>
Co-authored-by: Cyril Cohen <cohen@crans.org>
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
---
 CHANGELOG_UNRELEASED.md  |  6 ++++++
 classical/set_interval.v | 19 +++++++++++++++++--
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index edc9ba4cf3..399f8064a6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -86,6 +86,9 @@
            `le0_nondecreasing_set_nonincreasing_integral`,
 	   `le0_nondecreasing_set_cvg_integral`
 
+- in `set_interval.v`:
+  + lemma `memB_itv`, `memB_itv0`
+
 ### Changed
 
 - in `convex.v`:
@@ -236,6 +239,9 @@
 
 ### Deprecated
 
+- in `set_interval.v`:
+  + lemma `mem_1B_itvcc`
+
 ### Removed
 
 - in `measure.v`:
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 30ec1947ea..0f7b5392db 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -535,8 +535,21 @@ Section line_path_factor_numDomainType.
 Variable R : numDomainType.
 Implicit Types (a b t r : R) (A : set R).
 
-Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).
-Proof. by rewrite !in_itv/= subr_ge0 gerDl oppr_le0 andbC. Qed.
+Lemma memB_itv (x y : bool) a b t :
+  (b - t \in Interval (BSide x a) (BSide y b)) =
+  (a + t \in Interval (BSide (~~ y) a) (BSide (~~ x) b)).
+Proof.
+rewrite !in_itv/= /Order.lteif !if_neg.
+by rewrite gerBl gtrBl lerDl ltrDl lerBrDr ltrBrDr andbC.
+Qed.
+
+Lemma memB_itv0 (x y : bool) (a b : R) :
+  (b - a \in Interval (BSide x 0) (BSide y b)) =
+  (a \in Interval (BSide (~~ y) 0) (BSide (~~ x) b)).
+Proof. by rewrite memB_itv add0r. Qed.
+
+Lemma __deprepcated__mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).
+Proof. exact: memB_itv0. Qed.
 
 Definition line_path a b t : R := (1 - t) * a + t * b.
 
@@ -591,6 +604,8 @@ Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b.
 Proof. by []. Qed.
 
 End line_path_factor_numDomainType.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="use to `memB_itv0` instead")]
+Notation mem_1B_itvcc := __deprepcated__mem_1B_itvcc (only parsing).
 
 Section line_path_factor_numFieldType.
 Variable R : numFieldType.

From 649b5cf64551be68fe46bde0bdffb4c1611e3cc8 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Tue, 24 Jun 2025 22:29:22 +0900
Subject: [PATCH 2/2] Update classical/set_interval.v

---
 classical/set_interval.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/classical/set_interval.v b/classical/set_interval.v
index 0f7b5392db..5cda86b556 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -604,7 +604,7 @@ Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b.
 Proof. by []. Qed.
 
 End line_path_factor_numDomainType.
-#[deprecated(since="mathcomp-analysis 1.12.0", note="use to `memB_itv0` instead")]
+#[deprecated(since="mathcomp-analysis 1.12.0", note="use `memB_itv0` instead")]
 Notation mem_1B_itvcc := __deprepcated__mem_1B_itvcc (only parsing).
 
 Section line_path_factor_numFieldType.