From c2689b63f30c709de2e8d12b07c185c330480328 Mon Sep 17 00:00:00 2001
From: Arthur Azevedo de Amorim <arthur.aa@gmail.com>
Date: Mon, 12 May 2025 06:10:25 -0400
Subject: [PATCH] Add lemma finsupp_fsfun.

---
 finmap.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/finmap.v b/finmap.v
index 80bac9d..ed3d29e 100644
--- a/finmap.v
+++ b/finmap.v
@@ -3996,6 +3996,14 @@ Proof. by move=> x; rewrite unlock insubF ?inE. Qed.
 
 Definition fsfunE := (fsfun_fun, fsfun0E).
 
+Lemma finsupp_fsfun (S : {fset K}) h :
+  finsupp [fsfun[key] a : S => h (\val a) | default a]
+  = [fset x | x in S & h x != default x].
+Proof.
+apply/fsetP=> x; rewrite mem_finsupp fsfunE inE /= inE.
+by case: ifP => // _; rewrite eqxx.
+Qed.
+
 Lemma finsupp_sub  (S : {fset K}) (h : S -> V) :
   finsupp [fsfun[key] a : S => h a | default a] `<=` S.
 Proof.