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.