5 files changed, 52 insertions, 6 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 720bdd4af5..f696ff0754 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -810,6 +810,18 @@ Module Properties (M: S).
     apply H0; 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 cardinal_1 : forall (m:t elt), Empty m -> cardinal m = 0.
   Proof.
     intros; rewrite <- cardinal_Empty; auto.
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) ->
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 5ff52495af..25187da6d2 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -496,9 +496,9 @@ Qed.
 (** Properties of [fold] *)
 
 Lemma exclusive_set : forall s s' x,
- ~In x s\/~In x s' <-> mem x s && mem x s'=false.
+ ~(In x s/\In x s') <-> mem x s && mem x s'=false.
 Proof.
-intros; do 2 rewrite not_mem_iff.
+intros; do 2 rewrite mem_iff.
 destruct (mem x s); destruct (mem x s'); intuition.
 Qed.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index f6eebdc177..c2d69b9d24 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -640,6 +640,16 @@ Module Properties (M: S).
     exists e; auto.
   Qed.
 
+  Lemma cardinal_inv_2b :
+   forall s, cardinal s <> 0 -> { x : elt | In x s }.
+  Proof.
+    intros; rewrite M.cardinal_1 in H.
+    generalize (elements_2 (s:=s)).
+    destruct (elements s); simpl in H.
+    elim H; auto.
+    exists e; auto.
+  Qed.
+
   Lemma cardinal_1 : forall s, Empty s -> cardinal s = 0.
   Proof.
     intros. rewrite <- cardinal_Empty; auto.
@@ -950,7 +960,8 @@ Module Properties (M: S).
   apply fold_1; auto with set.
   Qed.
 
-  Lemma fold_union: forall i s s', (forall x, ~In x s\/~In x s') ->
+  Lemma fold_union: forall i s s', 
+   (forall x, ~(In x s/\In x s')) ->
    eqA (fold f (union s s') i) (fold f s (fold f s' i)).
   Proof.
   intros.
@@ -1005,7 +1016,7 @@ Module Properties (M: S).
   Qed.
 
   Lemma union_cardinal: 
-   forall s s', (forall x, ~In x s\/~In x s') -> 
+   forall s s', (forall x, ~(In x s/\In x s')) -> 
    cardinal (union s s')=cardinal s+cardinal s'.
   Proof.
   intros; do 3 rewrite cardinal_fold.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index fa04b4fbfb..bf7f3639c4 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -567,6 +567,16 @@ Module Properties
     exists e; auto.
   Qed.
 
+  Lemma cardinal_inv_2b :
+   forall s, cardinal s <> 0 -> { x : elt | In x s }.
+  Proof.
+    intros; rewrite M.cardinal_1 in H.
+    generalize (elements_2 (s:=s)).
+    destruct (elements s); simpl in H.
+    elim H; auto.
+    exists e; auto.
+  Qed.
+
   Lemma Equal_cardinal_aux :
    forall n s s', cardinal s = n -> s[=]s' -> cardinal s = cardinal s'.
   Proof.
@@ -761,7 +771,8 @@ Module Properties
   apply fold_1; auto with set.
   Qed.
 
-  Lemma fold_union: forall s s', (forall x, ~In x s\/~In x s') ->
+  Lemma fold_union: forall s s', 
+   (forall x, ~(In x s/\In x s')) ->
    eqA (fold f (union s s') i) (fold f s (fold f s' i)).
   Proof.
   intros.
@@ -821,7 +832,7 @@ Module Properties
   Qed.
 
   Lemma union_cardinal: 
-   forall s s', (forall x, ~In x s\/~In x s') -> 
+   forall s s', (forall x, ~(In x s/\In x s')) -> 
    cardinal (union s s')=cardinal s+cardinal s'.
   Proof.
   intros; do 3 rewrite cardinal_fold.