fix combining two q/2 fractions to a q

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

tests/proofmode_iris.v

 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.

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.