diff --git a/tests/solve_ndisj.ref b/tests/solve_ndisj.ref
index 64a2dc8e334bfc8384132fbf5279262a9c644181..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/tests/solve_ndisj.ref
+++ b/tests/solve_ndisj.ref
@@ -1,3 +0,0 @@
-The command has indeed failed with message:
-Ltac call to "solve_ndisj" failed.
-No applicable tactic.
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 7a58ba3acafebc142888767f88d952357e1468b1..3774753969a307d0d8196c80d6c094c64f82b544 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -1,7 +1,5 @@
 From stdpp Require Import namespaces strings.
 
-Set Ltac Backtrace.
-
 Lemma test1 (N1 N2 : namespace) :
   N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
 Proof. solve_ndisj. Qed.
@@ -20,9 +18,4 @@ Proof. solve_ndisj. Qed.
 
 Lemma test5 (N1 N2 : namespace) :
   ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
-Proof.
-  Fail solve_ndisj. (* FIXME: it should be able to solve this. *)
-  apply namespace_subseteq_difference.
-  { apply ndot_preserve_disjoint_r. set_solver. }
-  solve_ndisj.
-Qed.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 38862b12ea38778ce606143cbc2f769e7c9ad2f9..04f9e931143bac93cd0465fcf847f923f23aedde 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -66,35 +66,37 @@ Section namespace.
 
   Lemma ndot_preserve_disjoint_r N E x : E ## ↑N → E ## ↑N.@x.
   Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
-
-  Lemma namespace_subseteq_difference E1 E2 E3 :
-    E1 ## E3 → E1 ⊆ E2 → E1 ⊆ E2 ∖ E3.
-  Proof. set_solver. Qed.
-
-  Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 ⊆ E3 → E1 ∖ E2 ⊆ E3.
-  Proof. set_solver. Qed.
-
-  Lemma ndisj_difference_l E N1 N2 : ↑N2 ⊆ (↑N1 : coPset) → E ∖ ↑N1 ## ↑N2.
-  Proof. set_solver. Qed.
 End namespace.
 
-(* The hope is that registering these will suffice to solve most goals
+(** The hope is that registering these will suffice to solve most goals
 of the forms:
 - [N1 ## N2]
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
 Create HintDb ndisj.
-Hint Resolve namespace_subseteq_difference : ndisj.
-Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
-Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
-Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
-Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
+
+(** Rules for goals of the form [_ ⊆ _] *)
+(** If-and-only-if rules. Well, not quite, but for the fragment we are
+considering they are. *)
+Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
+(** Fallback, loses lots of information but lets other rules make progress. *)
+Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
+Hint Resolve nclose_subseteq' | 100 : ndisj.
+
+(** Rules for goals of the form [_ ## _] *)
+(** The base rule that we want to ultimately get down to. *)
+Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
+(** Fallback, loses lots of information but lets other rules make progress.
+Tests show trying [disjoint_difference_l1] first gives better performance. *)
+Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj.
+Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.
+Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with
   | H : _ ∪ _ ⊆ _ |- _ => apply union_subseteq in H as [??]
   end;
-  solve [eauto 10 with ndisj].
+  solve [eauto 12 with ndisj].
 Hint Extern 1000 => solve_ndisj : solve_ndisj.
diff --git a/theories/sets.v b/theories/sets.v
index 90aeda1f5ab5d5a33569d0e4255630ceaee3116f..015b98d6843358dcdcfeedd90145161a93d1c9da 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -653,9 +653,23 @@ Section set.
   Lemma difference_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y.
   Proof. set_solver. Qed.
 
+  Lemma subseteq_difference_r X Y1 Y2 :
+    X ## Y2 → X ⊆ Y1 → X ⊆ Y1 ∖ Y2.
+  Proof. set_solver. Qed.
+  Lemma subseteq_difference_l X1 X2 Y : X1 ⊆ Y → X1 ∖ X2 ⊆ Y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma disjoint_intersection X Y : X ## Y ↔ X ∩ Y ≡ ∅.
   Proof. set_solver. Qed.
+  Lemma disjoint_difference_l1 X1 X2 Y : Y ⊆ X2 → X1 ∖ X2 ## Y.
+  Proof. set_solver. Qed.
+  Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y → X1 ∖ X2 ## Y.
+  Proof. set_solver. Qed.
+  Lemma disjoint_difference_r1 X Y1 Y2 : X ⊆ Y2 → X ## Y1 ∖ Y2.
+  Proof. set_solver. Qed.
+  Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1 → X ## Y1 ∖ Y2.
+  Proof. set_solver. Qed.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.