diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 09ec793416c260a163cb75646320e1babb9d8e45..fee607f8ac991992c64fb3828008d8826d112bc5 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.