From 8980313c9785370752b8b5c0ba4fdf1e9c3dc52f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 20 Nov 2025 11:23:29 +0900
Subject: [PATCH 01/11] characterization of limit_point using infinite_set

---
 CHANGELOG_UNRELEASED.md                    |  3 ++
 theories/normedtype_theory/normed_module.v | 62 ++++++++++++++++++++++
 2 files changed, 65 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9d62882c7b..23b4ca1b57 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,9 @@
 - in `convex.v`:
   + lemmas `convN`, `conv_le`
 
+- in `normed_module.v`:
+  + lemma `limit_point_infinite_setP`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 7defc3e494..7a70db7e19 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1036,6 +1036,68 @@ move=> n; have : nbhs (x : T) (U n).
 by move/Ax/cid => [/= an [anx Aan Uan]]; exists an.
 Unshelve. all: by end_near. Qed.
 
+Lemma limit_point_infinite_setP {R : archiRealFieldType} (E : set R) (a : R) :
+  limit_point E a <-> (forall U, nbhs a U -> infinite_set (U `&` E)).
+Proof.
+split=> [Ea V aV|]; last first.
+  move=> aE U /aE /infiniteP /pcard_leP /injfunPex[/= f funf injf].
+  have [f0a|f0a] := eqVneq (f O) a; last first.
+    by exists (f 0); have /= [Uf0 Ef0]:= funf 0 Logic.I.
+  have /= [Uf1 Ef1]:= funf 1 Logic.I.
+  exists (f 1); split => //; apply/eqP => f1a.
+  have := injf 1 0 (in_setT _) (in_setT _).
+  by rewrite f1a f0a => /(_ erefl); exact/eqP/oner_neq0.
+(* we build 2 sequences a_ and r_ s.t. a_i and r_i have the properties: *)
+pose elt_prop (ar : R * R) := [/\ ball a ar.2 `<=` V,
+  ar.1 \in E, ar.1 \in (ball a ar.2 : set R), ar.2 > 0 & ar.1 != a].
+pose elt_type := {ar : R * R | elt_prop ar}.
+pose a_ (x : elt_type) := (proj1_sig x).2.
+pose r_ (x : elt_type) := (proj1_sig x).1.
+(* two successive (a_i, r_i) and (a_j, r_j) satisfy the relation: *)
+pose elt_rel i j := `|a - r_ i| = a_ j /\ ball a (a_ j) `<=` ball a (a_ i) /\
+  `|a - r_ j| < `|a - r_ i| /\ r_ i != r_ j.
+move: aV => -[r0/= r0_gt0 ar0V].
+pose V0 : set R := ball a r0.
+move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
+have [a0 [a0a a0V0 a0E]] : exists a0, [/\ a0 != a, a0 \in V0 & a0 \in E].
+  move/cvgrPdist_lt : y_cvg_a => /(_ _ r0_gt0)[M _ May_r0].
+  exists (y_ M); split => //.
+  - by apply/mem_set; rewrite /V0 /ball/= May_r0/=.
+  - by apply/mem_set/y_E; exists M.
+have [v [v0 Pv]] : {v : nat -> elt_type |
+    v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
+    forall n, elt_rel (v n) (v n.+1)}.
+  apply: dependent_choice => -[[ai ri] [/= ariV xE aiari ri_gt0 aia]].
+  pose rj : R := `|a - ai|.
+  have rj_gt0 : 0 < rj by rewrite /rj normr_gt0 subr_eq0 eq_sym.
+  apply/cid; move/cvgrPdist_lt : y_cvg_a => /(_ _ rj_gt0)[M/= _ May_rj].
+  pose Vj : set R := ball a rj.
+  have VjV : Vj `<=` V.
+    apply: subset_trans ariV => z /lt_le_trans; apply.
+    by move: aiari; rewrite inE /ball/= => /ltW.
+  have y_MVj : y_ M \in Vj.
+    rewrite inE /Vj /ball/= /rj (@lt_le_trans _ _ rj)//.
+    by apply: May_rj => /=.
+  have y_ME : y_ M \in E by rewrite inE; apply: y_E; exists M.
+  exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.
+  split; first exact.
+  split; rewrite /a_ /r_/=.
+    by apply: le_ball; move: aiari; rewrite inE /ball/= => /ltW.
+  split; first by move: y_MVj; rewrite inE.
+  by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
+apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).
+  move=> n _; rewrite /r_ /=.
+  case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem aiari _ _].
+  by split => //; exact: ariV.
+have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
+  elim: q p => [[]//|q ih p].
+  rewrite ltnS leq_eqVlt => /predU1P[ ->|/ih].
+    by case: (Pv q) => _ [] _ [].
+  by apply: le_lt_trans; case: (Pv q) => _ [] _ [] /ltW.
+move=> p q _ _ /=; apply: contraPP => /eqP.
+by rewrite neq_lt => /orP[] /arv; rewrite ltNge => /negP + H; apply; rewrite H.
+Unshelve. all: by end_near. Qed.
+
 Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f ->
   limn (EFin \o f) = (limn f)%:E.
 Proof.

From 9df49cf74dc049a442c918847a910f456a4b2322 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:04:05 +0900
Subject: [PATCH 02/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 7a70db7e19..fdf5e1828f 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1042,8 +1042,8 @@ Proof.
 split=> [Ea V aV|]; last first.
   move=> aE U /aE /infiniteP /pcard_leP /injfunPex[/= f funf injf].
   have [f0a|f0a] := eqVneq (f O) a; last first.
-    by exists (f 0); have /= [Uf0 Ef0]:= funf 0 Logic.I.
-  have /= [Uf1 Ef1]:= funf 1 Logic.I.
+    by exists (f 0); case: (funf 0 Logic.I).
+  have [Uf1 Ef1]:= funf 1 Logic.I.
   exists (f 1); split => //; apply/eqP => f1a.
   have := injf 1 0 (in_setT _) (in_setT _).
   by rewrite f1a f0a => /(_ erefl); exact/eqP/oner_neq0.

From a770007020012fe079937f2c280660c60f541976 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:05:30 +0900
Subject: [PATCH 03/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index fdf5e1828f..5bad1b01d3 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1044,7 +1044,7 @@ split=> [Ea V aV|]; last first.
   have [f0a|f0a] := eqVneq (f O) a; last first.
     by exists (f 0); case: (funf 0 Logic.I).
   have [Uf1 Ef1]:= funf 1 Logic.I.
-  exists (f 1); split => //; apply/eqP => f1a.
+  exists (f 1); split=> //; apply/eqP => f1a.
   have := injf 1 0 (in_setT _) (in_setT _).
   by rewrite f1a f0a => /(_ erefl); exact/eqP/oner_neq0.
 (* we build 2 sequences a_ and r_ s.t. a_i and r_i have the properties: *)

From 6a3016f3a711e7db58c524e073a9545b6929ab41 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:08:00 +0900
Subject: [PATCH 04/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 5bad1b01d3..d177bb42f6 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1061,7 +1061,7 @@ pose V0 : set R := ball a r0.
 move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
 have [a0 [a0a a0V0 a0E]] : exists a0, [/\ a0 != a, a0 \in V0 & a0 \in E].
   move/cvgrPdist_lt : y_cvg_a => /(_ _ r0_gt0)[M _ May_r0].
-  exists (y_ M); split => //.
+  exists (y_ M); split=> //.
   - by apply/mem_set; rewrite /V0 /ball/= May_r0/=.
   - by apply/mem_set/y_E; exists M.
 have [v [v0 Pv]] : {v : nat -> elt_type |

From c8093b92d72992c6137919c2e3b6d74ad85e8baf Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:08:40 +0900
Subject: [PATCH 05/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index d177bb42f6..844ec6c346 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1062,8 +1062,8 @@ move/limit_pointP : Ea => [y_ [y_E y_neq_a y_cvg_a]].
 have [a0 [a0a a0V0 a0E]] : exists a0, [/\ a0 != a, a0 \in V0 & a0 \in E].
   move/cvgrPdist_lt : y_cvg_a => /(_ _ r0_gt0)[M _ May_r0].
   exists (y_ M); split=> //.
-  - by apply/mem_set; rewrite /V0 /ball/= May_r0/=.
-  - by apply/mem_set/y_E; exists M.
+  - by apply/mem_set/May_r0 => /=.
+  - by apply/mem_set/y_E/imageT.
 have [v [v0 Pv]] : {v : nat -> elt_type |
     v 0 = exist _ (a0, r0) (And5 ar0V a0E a0V0 r0_gt0 a0a) /\
     forall n, elt_rel (v n) (v n.+1)}.

From b0cbefa322e1a61b08eadee28960ab90da36bab7 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:11:31 +0900
Subject: [PATCH 06/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 844ec6c346..067c4f9749 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1073,16 +1073,16 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
   apply/cid; move/cvgrPdist_lt : y_cvg_a => /(_ _ rj_gt0)[M/= _ May_rj].
   pose Vj : set R := ball a rj.
   have VjV : Vj `<=` V.
-    apply: subset_trans ariV => z /lt_le_trans; apply.
-    by move: aiari; rewrite inE /ball/= => /ltW.
+    apply: subset_trans ariV => z /lt_trans; apply.
+    by move: aiari; rewrite inE.
   have y_MVj : y_ M \in Vj.
-    rewrite inE /Vj /ball/= /rj (@lt_le_trans _ _ rj)//.
+    rewrite inE; apply: (@lt_le_trans _ _ rj)//.
     by apply: May_rj => /=.
-  have y_ME : y_ M \in E by rewrite inE; apply: y_E; exists M.
+  have y_ME : y_ M \in E by rewrite inE; apply/y_E/imageT.
   exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.
   split; first exact.
   split; rewrite /a_ /r_/=.
-    by apply: le_ball; move: aiari; rewrite inE /ball/= => /ltW.
+    by apply: le_ball; move: aiari; rewrite inE => /ltW.
   split; first by move: y_MVj; rewrite inE.
   by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
 apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).

From 57aa839f1a20ba5aac513e28b9bcc1f87af24b42 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:11:44 +0900
Subject: [PATCH 07/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 067c4f9749..80a0a9c14f 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1087,8 +1087,7 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
   by apply/eqP => aiyM; move: y_MVj; rewrite -aiyM inE /Vj /ball/= /rj ltxx.
 apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).
   move=> n _; rewrite /r_ /=.
-  case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem aiari _ _].
-  by split => //; exact: ariV.
+  by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
 have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
   elim: q p => [[]//|q ih p].
   rewrite ltnS leq_eqVlt => /predU1P[ ->|/ih].

From 7fa05d72b2c30976c2dc5b47aa3daed389cd8a45 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:12:11 +0900
Subject: [PATCH 08/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 80a0a9c14f..4c3e45734f 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1090,9 +1090,8 @@ apply/infiniteP/pcard_leP/injfunPex => /=; exists (r_ \o v).
   by case: (v n) => -[ai ri] [/= ariV /set_mem Eai /set_mem/ariV aiari _ _].
 have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
   elim: q p => [[]//|q ih p].
-  rewrite ltnS leq_eqVlt => /predU1P[ ->|/ih].
+  by rewrite ltnS leq_eqVlt => /predU1P[->|/ih]; last apply: lt_trans;
     by case: (Pv q) => _ [] _ [].
-  by apply: le_lt_trans; case: (Pv q) => _ [] _ [] /ltW.
 move=> p q _ _ /=; apply: contraPP => /eqP.
 by rewrite neq_lt => /orP[] /arv; rewrite ltNge => /negP + H; apply; rewrite H.
 Unshelve. all: by end_near. Qed.

From 2d36e3f6d43e2cda04bdc9e5ad244a965259614c Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:12:27 +0900
Subject: [PATCH 09/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 4c3e45734f..249c4e1b9a 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1093,7 +1093,7 @@ have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
   by rewrite ltnS leq_eqVlt => /predU1P[->|/ih]; last apply: lt_trans;
     by case: (Pv q) => _ [] _ [].
 move=> p q _ _ /=; apply: contraPP => /eqP.
-by rewrite neq_lt => /orP[] /arv; rewrite ltNge => /negP + H; apply; rewrite H.
+by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx.
 Unshelve. all: by end_near. Qed.
 
 Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f ->

From d51186cb2a0f439896f23aae84611488a1601c70 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Nov 2025 17:12:47 +0900
Subject: [PATCH 10/11] Update theories/normedtype_theory/normed_module.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>
---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 249c4e1b9a..89d0f3efe9 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1094,7 +1094,7 @@ have arv q p : (p < q)%N -> `|a - r_ (v q)| < `|a - r_ (v p)|.
     by case: (Pv q) => _ [] _ [].
 move=> p q _ _ /=; apply: contraPP => /eqP.
 by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx.
-Unshelve. all: by end_near. Qed.
+Qed.
 
 Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f ->
   limn (EFin \o f) = (limn f)%:E.

From b69bff8c13d0ed029a5362b559c962a6fb861c2e Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 21 Nov 2025 19:56:00 +0900
Subject: [PATCH 11/11] fix

---
 theories/normedtype_theory/normed_module.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 89d0f3efe9..7cd8a6f9e9 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -1076,7 +1076,7 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
     apply: subset_trans ariV => z /lt_trans; apply.
     by move: aiari; rewrite inE.
   have y_MVj : y_ M \in Vj.
-    rewrite inE; apply: (@lt_le_trans _ _ rj)//.
+    rewrite inE; apply: (@lt_le_trans _ _ rj) => //.
     by apply: May_rj => /=.
   have y_ME : y_ M \in E by rewrite inE; apply/y_E/imageT.
   exists (exist _ (y_ M, rj) (And5 VjV y_ME y_MVj rj_gt0 (y_neq_a M))) => /=.