diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 349be4dfd622c941d4f5e0fbcbd64a3af77ef059..751285832e74e5e957e0d1133c4cf28e0f655f61 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -163,7 +163,7 @@ Section positive.
   Local Instance pos_validN_instance : ValidN positive := λ n x, True.
   Local Instance pos_pcore_instance : PCore positive := λ x, None.
   Local Instance pos_op_instance : Op positive := Pos.add.
-  Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
+  Definition pos_op_add x y : x â‹… y = (x + y)%positive := eq_refl.
   Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
   Proof. by rewrite Plt_sum. Qed.
   Lemma pos_ra_mixin : RAMixin positive.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 70f0dd6b0d1fa0a8465646e5279028db9d4ae573..4828ebcd58afccefcdcaab634c25a15904b32298 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -183,7 +183,7 @@ Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
 Proof. done. Qed.
 Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
 Proof. induction n; f_equiv/=; auto. Qed.
-Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
+Lemma laterN_add n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
 Proof. induction n1; f_equiv/=; auto. Qed.
 Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
 Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 3d4ba827644d1cc9d8bb12e1d147cf0c13bf5567..2fc06fa62d672b97106395460bf509a6c6886536 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -288,7 +288,7 @@ Global Instance into_laterN_later only_head n n' m' P Q lQ :
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
   move=> Hn [_ ->|->] <-;
-    by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
+    by rewrite -later_laterN -laterN_add -Hn Nat.add_comm.
 Qed.
 Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
   NatCancel n m n' m' →
@@ -297,7 +297,7 @@ Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
   IntoLaterN only_head n (â–·^m P) lQ | 1.
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
-  move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
+  move=> Hn [_ ->|->] <-; by rewrite -!laterN_add -Hn Nat.add_comm.
 Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :