diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 9cbbce1b7e71dea57196fe5676091208b0bb93e1..100a162b6be4e8a282c90beb434c3e82b38346cb 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -115,6 +115,35 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
+"test_frac_split_combine"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  inG0 : inG Σ fracR
+  γ : gname
+  ============================
+  "H1" : own γ (1 / 2)%Qp
+  "H2" : own γ (1 / 2)%Qp
+  --------------------------------------∗
+  own γ 1%Qp
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  inG0 : inG Σ fracR
+  γ : gname
+  ============================
+  "H" : own γ 1%Qp
+  --------------------------------------∗
+  own γ 1%Qp
+  
 "test_iInv"
      : string
 1 subgoal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 416707464aa0083706188a93dc82f3f452f646c8..e3e5102007459276eb9b88844bb4c6180599eff6 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics monpred.
+From iris.algebra Require Import frac.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
@@ -236,6 +237,16 @@ Section iris_tests.
     x' ≼ x →
     own γ x -∗ own γ x'.
   Proof. intros. by iApply own_mono. Qed.
+
+  Check "test_frac_split_combine".
+  Lemma test_frac_split_combine `{!inG Σ fracR} γ :
+    own γ 1%Qp -∗ own γ 1%Qp.
+  Proof.
+    iIntros "[H1 H2]". Show.
+    iCombine "H1 H2" as "H". Show.
+    iExact "H".
+  Qed.
+
 End iris_tests.
 
 Section monpred_tests.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 4fea0470c2e74174a746630034789f0c15b12890..017254200c3d814df533af8e1f99c6dd12872320 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -60,5 +60,5 @@ Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
 
 (* This one has a higher precendence than [is_op_op] so we get a [+] instead
    of an [â‹…]. *)
-Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2.
+Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
 Proof. done. Qed.