From b324dd7d84c73d42fc93d324098dc86021b34ad5 Mon Sep 17 00:00:00 2001
From: amethyst <yosukeito@itouyouukenoAir.lan>
Date: Sun, 11 Aug 2024 13:11:47 +0900
Subject: [PATCH] Add-Lemma_not_near_ninftyP

---
 CHANGELOG_UNRELEASED.md |  2 ++
 theories/normedtype.v   | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 698794d56..414e498f5 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,6 +3,8 @@
 ## [Unreleased]
 
 ### Added
+- in `normedtype.v`:
+  + lemmas `not_near_inftyP` `not_near_ninftyP`
 
 ### Changed
 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 98739bc33..a067e9453 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -428,6 +428,24 @@ move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM.
 by move=> x; rewrite -ltr_pdivlMr //; exact: AM.
 Qed.
 
+Lemma not_near_inftyP T (f : R -> T) (P : pred T):
+  ~ (\forall x \near +oo, P (f x)) <->
+    forall M : R, M \is Num.real -> exists2 x, M < x & ~ P (f x).
+Proof.
+rewrite nearE /ninfty_nbhs -forallNP.
+rewrite -propeqE; apply: eq_forall => M; rewrite propeqE.
+by rewrite -implypN existsPNP.
+Qed.
+
+Lemma not_near_ninftyP T (f : R -> T) (P : pred T):
+  ~ (\forall x \near -oo, P (f x)) <->
+    forall M : R, M \is Num.real -> exists2 x, x < M & ~ P (f x).
+Proof.
+rewrite nearE /ninfty_nbhs -forallNP.
+rewrite -propeqE; apply: eq_forall => M; rewrite propeqE.
+by rewrite -implypN existsPNP.
+Qed.
+
 End infty_nbhs_instances.
 
 #[global] Hint Extern 0 (is_true (_ < ?x)) => match goal with