solve_ndisj: solve more goals involving chains of differences

This improves solve_ndisj to handle goals that came up in iris/examples as part of the logically atomic triple mask change.

tests/solve_ndisj.v

@@ -35,3 +35,11 @@ Proof. solve_ndisj. Qed.
 Lemma test7 N :
   ↑N ⊆@{coPset} ⊤ ∖ ∅.
 Proof. solve_ndisj. Qed.
+
+Lemma test8 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter".
+Proof. solve_ndisj. Qed.
+
+Lemma test9 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
+Proof. solve_ndisj. Qed.