petits ajouts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index f53e1d2b5c..af8dccf536 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -326,6 +326,22 @@ rewrite <- H0; rewrite H2; rewrite H1; auto.
 auto.
 Qed.
 
+Lemma empty_o : forall x, find x (empty elt) = None.
+Proof.
+intros.
+case_eq (find x (empty elt)); intros; auto.
+generalize (find_2 H).
+rewrite empty_mapsto_iff; intuition.
+Qed.
+
+Lemma empty_a : forall x, mem x (empty elt) = false.
+Proof.
+intros.
+case_eq (mem x (empty elt)); intros; auto.
+generalize (mem_2 H).
+rewrite empty_in_iff; intuition.
+Qed.
+
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.