From 31ced05457bc6f83ce74eaa328aa99f8257fa0e3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 5 Mar 2026 18:36:43 +0900
Subject: [PATCH] add lt_nbhs{r,l} variants

- fixes #1879
---
 CHANGELOG_UNRELEASED.md                 |  6 ++++++
 theories/topology_theory/num_topology.v | 10 +++++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5b7f660af6..10ace17990 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -70,6 +70,9 @@
 - in `derive.v`:
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
+- in `num_topology.v`:
+  + lemmas `lt_le_nbhsr`, `lt_le_nbhsl`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.
@@ -251,6 +254,9 @@
   + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
     `integral_itv_bndoo`
 
+- in `num_topology.v`:
+  + lemma `lt_nbhsl`
+
 ### Deprecated
 
 - in `lebesgue_integral_nonneg.v`:
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 415e7c0ee6..94980019c2 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -374,7 +374,7 @@ exists x => // z /=; rewrite sub0r normrN.
 by apply: le_lt_trans; rewrite ler_norm.
 Qed.
 
-Lemma lt_nbhsl {R : realType} (x a : R) : x < a ->
+Lemma lt_nbhsl {R : realFieldType} (x a : R) : x < a ->
   \forall y \near nbhs x, y < a.
 Proof.
 move=> xb; exists ((a - x) / 2) => /=; first by rewrite divr_gt0// subr_gt0.
@@ -382,6 +382,10 @@ move=> r/=; rewrite ltr_pdivlMr// ltrBrDr; apply: le_lt_trans.
 by rewrite -lerBlDr -normrN opprB (le_trans (ler_norm _))// ler_peMr// ler1n.
 Qed.
 
+Lemma lt_le_nbhsl {R : realFieldType} (t x : R) :
+  x < t -> \forall y \near nbhs x, y <= t.
+Proof. by move/lt_nbhsl; apply: filterS => y /ltW. Qed.
+
 Lemma Nlt_nbhsl {R : realType} (x a : R) :
   - x < a -> \forall y \near nbhs x, - y < a.
 Proof.
@@ -426,6 +430,10 @@ have [uz|uz] := leP u z.
 by rewrite ltr0_norm ?subr_lt0// opprB addrAC -lerBlDr opprK lerD// ?ltW.
 Qed.
 
+Lemma lt_le_nbhsr {R : realFieldType} (t x : R) :
+  t < x -> \forall y \near nbhs x, t <= y.
+Proof. by move/lt_nbhsr; apply: filterS => y /ltW. Qed.
+
 Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) :
   ProperFilter x^'.
 Proof.