From eef661f36045a678ca126edf29fa6f973a3e00e1 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 1 Jan 2026 12:20:30 +0900
Subject: [PATCH] from MathComp-Analysis' unstable.v

---
 CHANGELOG_UNRELEASED.md | 3 +++
 finmap.v                | 9 +++++++++
 2 files changed, 12 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 340789c..a5cbca3 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -7,6 +7,9 @@
 - in `finmap.v`:
   + lemma `card_fset_sum1`
 
+- in `finmap.v`:
+  + lemma `fset_nat_maximum`
+
 ### Changed
 
 ### Renamed
diff --git a/finmap.v b/finmap.v
index ad60625..98148ae 100644
--- a/finmap.v
+++ b/finmap.v
@@ -1800,6 +1800,15 @@ rewrite -cardfs_eq0 cardfE; apply: (equivP existsP).
 by split=> [] [a aP]; [exists (val a); apply: valP|exists [` aP]].
 Qed.
 
+Lemma fset_nat_maximum A (f : K -> nat) : A != fset0 ->
+  (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%N.
+Proof.
+move=> /fset0Pn[x Ax].
+have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT.
+exists (val y); split; first exact: valP.
+by move=> z Az; have := mf [` Az]%fset.
+Qed.
+
 Lemma cardfs_gt0 A : (0 < #|` A|)%N = (A != fset0).
 Proof. by rewrite lt0n cardfs_eq0. Qed.