From cdd8dd73a991e1e81ec718b75e47baa5d16cad41 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 3 Jul 2025 18:00:36 +0900
Subject: [PATCH] lemma from MathComp-Analysis' `unstable.v`

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

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bd..340789c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `finmap.v`:
+  + lemma `card_fset_sum1`
+
 ### Changed
 
 ### Renamed
diff --git a/finmap.v b/finmap.v
index 9484849..ad60625 100644
--- a/finmap.v
+++ b/finmap.v
@@ -2313,6 +2313,9 @@ Proof. by rewrite big_seq_fsetE big_fset1. Qed.
 
 End BigFSet.
 
+Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) : #|` A| = \sum_(i <- A) 1.
+Proof. by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.
+
 Notation eq_big_imfset := (perm_big _ (enum_imfset _ _)).
 
 Section BigComFSet.