diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 869e6e08413468566fe2206d23c6f50ed28a1883..6586c849b7767135e021286263a60c782669e6fe 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -404,6 +404,10 @@ Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
 Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
   IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
+(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
+an [â‹…]. *)
+Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+Proof. done. Qed.
 
 (* IntoAnd *)
 Global Instance into_and_sep p P Q : IntoAnd p (P ∗ Q) P Q.