diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index acd0190cfc8c6f8777034ec77f3ee2f7a40f6772..d63748060b0640ae4e175280a3ea45bbb7afe9c3 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -105,24 +105,26 @@ Section later_credit_theory.
     rewrite lc_unseal /lc_def. apply _.
   Qed.
 
+  (** Make sure that the rule for [+] is used before [S], otherwise Coq's
+  unification applies the [S] hint too eagerly. See Iris issue #470. *)
   Global Instance from_sep_lc_add n m :
-    FromSep (£ (n + m)) (£ n) (£ m).
+    FromSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /FromSep lc_split.
   Qed.
   Global Instance from_sep_lc_S n :
-    FromSep (£ (S n)) (£ 1) (£ n).
+    FromSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /FromSep (lc_succ n).
   Qed.
 
   Global Instance into_sep_lc_add n m :
-    IntoSep (£ (n + m)) (£ n) (£ m).
+    IntoSep (£ (n + m)) (£ n) (£ m) | 0.
   Proof.
     by rewrite /IntoSep lc_split.
   Qed.
   Global Instance into_sep_lc_S n :
-    IntoSep (£ (S n)) (£ 1) (£ n).
+    IntoSep (£ (S n)) (£ 1) (£ n) | 1.
   Proof.
     by rewrite /IntoSep (lc_succ n).
   Qed.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 4c4d3a96cccfc31df83059af42080a21c3d91ac8..229402b79781bad7359cb55b0a906ed47c778181 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -172,6 +172,38 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 The command has indeed failed with message:
 Tactic failure: iMod: "H" not fresh.
+"test_iIntros_lc"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  "Hlc2" : £ m
+  --------------------------------------∗
+  £ (S n)
+"lc_iSplit_lc"
+     : string
+2 goals
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  --------------------------------------∗
+  £ (S n)
+
+goal 2 is:
+ "Hlc2" : £ m
+ --------------------------------------∗
+ £ m
 "test_iInv"
      : string
 1 goal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 466099cd2894d91d28bf7bbd46a8d71ba42a314c..6884d140b88d0bafda214683ea802b88430cbabc 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -250,6 +250,15 @@ Section iris_tests.
     iIntros "H H'". Fail iDestruct "H'" as ">H".
   Abort.
 
+  (** Make sure that the splitting rule for [+] gets priority over the one for
+  [S]. See issue #470. *)
+  Check "test_iIntros_lc".
+  Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).
+  Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
+
+  Check "lc_iSplit_lc".
+  Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
+  Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
 End iris_tests.
 
 Section monpred_tests.