fix forgotten proof

math-comp · Aug 8, 2018 · ba023db · ba023db
1 parent 680e219
commit ba023db
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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.