From cce388fe968bc1450cfe3d16a83d24b8a067e0aa Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cyril.cohen@inria.fr>
Date: Wed, 5 Nov 2025 17:11:30 +0100
Subject: [PATCH] Missing fsubU1set lemma

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

diff --git a/finmap.v b/finmap.v
index ad60625..bbe2f14 100644
--- a/finmap.v
+++ b/finmap.v
@@ -1902,6 +1902,9 @@ apply/idP/idP => [subA|/andP [AB CA]]; last by rewrite -[A]fsetUid fsetUSS.
 by rewrite !(fsubset_trans _ subA).
 Qed.
 
+Lemma fsubU1set x A B : (x |` A `<=` B) = (x \in B) && (A `<=` B).
+Proof. by rewrite fsubUset fsub1set. Qed.
+
 Lemma fsubUsetP A B C : reflect (A `<=` C /\ B `<=` C) (A `|` B `<=` C).
 Proof. by rewrite fsubUset; exact: andP. Qed.