From ba023db33b3b16d53f9d7c6de2d91f3f7d75cc2b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 8 Aug 2018 08:47:45 +0200 Subject: [PATCH] fix forgotten proof --- set.v | 1 + 1 file changed, 1 insertion(+) diff --git a/set.v b/set.v index e7d6a21..10d2b3f 100644 --- a/set.v +++ b/set.v @@ -793,6 +793,7 @@ Lemma setU_eq0 A B : (A :|: B == set0) = (A == set0) && (B == set0). Proof. by rewrite -!subset0 subUset. Qed. Lemma setD_eq0 A B : (A :\: B == set0) = (A \subset B). +Proof. by rewrite -subset0 subDset setU0. Qed. Lemma subsetD1 A B x : (A \subset B :\ x) = (A \subset B) && (x \notin A). Proof.