Rename `laterN_plus` into `laterN_add`.

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.

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.

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 :