From 778fe88cc663103b2d16289ae18e075d45aa339f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 19 Jul 2021 12:25:18 +0200
Subject: [PATCH] more tests (by Robbert)

---
 tests/solve_ndisj.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 09ec7934..fee607f8 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -23,6 +23,11 @@ Lemma test5 N1 N2 :
   ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
 Proof. solve_ndisj. Qed.
 
+Lemma test_ndisjoint_difference_l N : ⊤ ∖ ↑N ##@{coPset} ↑N.
+Proof. solve_ndisj. Qed.
+Lemma test_ndisjoint_difference_r N : ↑N ##@{coPset} ⊤ ∖ ↑N.
+Proof. solve_ndisj. Qed.
+
 Lemma test6 E N :
   ↑N ⊆ E → ↑N ⊆ ⊤ ∖ (E ∖ ↑N).
 Proof. solve_ndisj. Qed.
-- 
GitLab