rm redundant lemma

math-comp · Aug 5, 2024 · 13d76d9 · 13d76d9
1 parent 73f8d11
commit 13d76d9
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 16 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -113,9 +113,6 @@
 - in `classical_sets.v`:
   + lemmas `xsectionP`, `ysectionP`
 
-- in `set_interval.v`:
-  + lemma `subset_itv_oo_ccW`
-
 - in `realfun.v`:
   + lemmas `nondecreasing_at_left_at_right`, `nonincreasing_at_left_at_right`
 

diff --git a/classical/set_interval.v b/classical/set_interval.v
@@ -207,13 +207,6 @@ move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->].
 by rewrite andbT; split => //; exact/nesym/eqP.
 Qed.
 
-Lemma subset_itv_oo_ccW x y u v : (u <= x)%O -> (y <= v)%O ->
-  `]x, y[ `<=` `[u, v].
-Proof.
-move=> ux yv; apply: (subset_trans _ (@subset_itv_oo_cc _ _ _ _)) => z/=.
-by rewrite !in_itv/= => /andP[? zy]; rewrite (le_lt_trans ux) ?(lt_le_trans zy).
-Qed.
-
 End set_itv_porderType.
 Arguments neitv {d T} _.
 

diff --git a/theories/realfun.v b/theories/realfun.v
@@ -386,11 +386,11 @@ Let nondecreasing_at_right_is_cvgrW f a b r : a < r -> r < b ->
 Proof.
 move=> ar rb ndf H; apply: nondecreasing_at_right_is_cvgr.
 - near=> s => x y xrs yrs xy; rewrite ndf//.
-  + by apply: subset_itv_oo_ccW xrs; exact/ltW.
-  + by apply: subset_itv_oo_ccW yrs; exact/ltW.
+  + by apply: subset_itvW xrs; exact/ltW.
+  + by apply: subset_itvW yrs; exact/ltW.
 - near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//.
   + by apply: subset_itv_oo_cc; rewrite in_itv/= ar.
-  + by apply: subset_itv_oo_ccW srx; exact/ltW.
+  + by apply: subset_itvW srx; exact/ltW.
   + by move: srx; rewrite in_itv/= => /andP[/ltW].
 Unshelve. all: by end_near. Qed.
 
@@ -399,10 +399,10 @@ Let nondecreasing_at_left_is_cvgrW f a b r : a < r -> r < b ->
 Proof.
 move=> ar rb ndf H; apply: nondecreasing_at_left_is_cvgr.
 - near=> s => x y xrs yrs xy; rewrite ndf//.
-  + by apply: subset_itv_oo_ccW xrs; exact/ltW.
-  + by apply: subset_itv_oo_ccW yrs; exact/ltW.
+  + by apply: subset_itvW xrs; exact/ltW.
+  + by apply: subset_itvW yrs; exact/ltW.
 - near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//.
-  + by apply: subset_itv_oo_ccW srx; exact/ltW.
+  + by apply: subset_itvW srx; exact/ltW.
   + by apply: subset_itv_oo_cc; rewrite in_itv/= ar.
   + by move: srx; rewrite in_itv/= => /andP[_ /ltW].
 Unshelve. all: by end_near. Qed.