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.