From e284a8bec3b4263596d058d193ab81d9f50b06dd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 4 Jan 2008 17:53:27 +0000
Subject: more user-friendly versions of some properties lemmas in FSets/FMap

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10420 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FMapWeakFacts.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'theories/FSets/FMapWeakFacts.v')

diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index 11608698fb..fbf761d8e5 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -725,6 +725,18 @@ Module Properties
   constructor; red; auto.
   Qed.
 
+  Lemma cardinal_inv_2b :
+   forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof. 
+    intros; unfold cardinal in *.
+    generalize (elements_2 (m:=m)).
+    destruct (elements m).
+    simpl in H; elim H; auto.
+    exists p; auto.
+    destruct p; simpl; auto.
+    apply H0; constructor; red; auto.
+  Qed.
+
   Lemma map_induction :
    forall P : t elt -> Type,
    (forall m, Empty m -> P m) ->
-- 
cgit v1.2.3