diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4edacb751ea954631b5b481f693b48e535dfd7a4..224d4dcbdb6892d2b0de6e2ab23a9e7220d49513 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,7 @@ lemma.
 * Remove `mono_list_lb_is_op` instance for `IsOp' (â—¯ML l) (â—¯ML l) (â—¯ML l)`; we
   don't usually have such instances for duplicable resources and it was added by
   accident.
+* Rename `pos_op_plus` into `pos_op_add`.
 
 **Changes in `bi`:**
 
@@ -53,6 +54,7 @@ lemma.
   `least_fixpoint_affine`, `least_fixpoint_absorbing`,
   `least_fixpoint_persistent_affine`, `least_fixpoint_persistent_absorbing`,
   `greatest_fixpoint_absorbing`.
+* Rename `laterN_plus` into `laterN_add`.
 
 **Changes in `proofmode`:**
 
@@ -151,6 +153,9 @@ s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
 s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
 # staging → unstable
 s/\biris\.staging\b/iris.unstable/g
+# plus → add
+s/\blaterN_plus\b/laterN_add/g
+s/\bpos_op_plus\b/pos_op_add/g
 EOF
 ```
 
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 :