diff --git a/stdpp/fin.v b/stdpp/fin.v
index 0701c7a7aff7c8bb3c7a07d725705af94fa340ca..a3d6aa1cfadc419de0edb0b1cd5f01169556efe7 100644
--- a/stdpp/fin.v
+++ b/stdpp/fin.v
@@ -87,26 +87,26 @@ Qed.
 Lemma nat_to_fin_to_nat {n} (i : fin n) H : @nat_to_fin (fin_to_nat i) n H = i.
 Proof. apply (inj fin_to_nat), fin_to_nat_to_fin. Qed.
 
-Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
+Fixpoint fin_add_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
     (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
     (H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
   match n1 with
   | 0 => λ P H1 H2 i, H2 i
-  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2)
+  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
   end.
 
-Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
+Lemma fin_add_inv_l {n1 n2} (P : fin (n1 + n2) → Type)
     (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) :
-  fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
+  fin_add_inv P H1 H2 (Fin.L n2 i) = H1 i.
 Proof.
   revert P H1 H2 i.
   induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
   intros i. apply (IH (λ i, P (FS i))).
 Qed.
 
-Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type)
+Lemma fin_add_inv_r {n1 n2} (P : fin (n1 + n2) → Type)
     (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) :
-  fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
+  fin_add_inv P H1 H2 (Fin.R n1 i) = H2 i.
 Proof.
   revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
   apply (IH (λ i, P (FS i))).
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index dabfc11ff6c9a3177cf339a3385f88694c5aecc4..99af32e6496d2a41ef25930c3e5322573f385b73 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -438,7 +438,7 @@ Section more_lemmas.
         by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
       rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
       rewrite (assoc_L _). f_equiv.
-      rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
+      rewrite (comm _); simpl. by rewrite replicate_add, Permutation_middle.
     - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
         by (by rewrite ?lookup_union_with, ?HX, ?HY).
       by rewrite <-(assoc_L (++)), <-IH.
diff --git a/stdpp/list.v b/stdpp/list.v
index 807dbc5b79b4a4ac28c43fc1d593b107c6162bae..2320e73e2250b96b7321eba6e29e7242f589aeeb 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -1244,7 +1244,7 @@ Lemma take_app3_alt l1 l2 l3 n : n = length l1 → take n ((l1 ++ l2) ++ l3) = l
 Proof. intros ->. by rewrite <-(assoc_L (++)), take_app. Qed.
 Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
 Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
-Lemma take_plus_app l k n m :
+Lemma take_add_app l k n m :
   length l = n → take (n + m) (l ++ k) = l ++ take m k.
 Proof. intros <-. induction l; f_equal/=; auto. Qed.
 Lemma take_app_ge l k n :
@@ -1339,7 +1339,7 @@ Proof.
   intros. rewrite <-(Nat.sub_add (length l) n) at 1 by done.
   by rewrite Nat.add_comm, <-drop_drop, drop_app.
 Qed.
-Lemma drop_plus_app l k n m :
+Lemma drop_add_app l k n m :
   length l = n → drop (n + m) (l ++ k) = drop m k.
 Proof. intros <-. by rewrite <-drop_drop, drop_app. Qed.
 Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
@@ -1438,7 +1438,7 @@ Lemma replicate_S n x : replicate (S n) x = x :: replicate  n x.
 Proof. done. Qed.
 Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
 Proof. induction n; f_equal/=; auto. Qed.
-Lemma replicate_plus n m x :
+Lemma replicate_add n m x :
   replicate (n + m) x = replicate n x ++ replicate m x.
 Proof. induction n; f_equal/=; auto. Qed.
 Lemma replicate_cons_app n x :
@@ -1446,11 +1446,11 @@ Lemma replicate_cons_app n x :
 Proof. induction n; f_equal/=; eauto.  Qed.
 Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
 Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
-Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
+Lemma take_replicate_add n m x : take n (replicate (n + m) x) = replicate n x.
 Proof. by rewrite take_replicate, min_l by lia. Qed.
 Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
 Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
-Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
+Lemma drop_replicate_add n m x : drop n (replicate (n + m) x) = replicate m x.
 Proof. rewrite drop_replicate. f_equal. lia. Qed.
 Lemma replicate_as_elem_of x n l :
   replicate n x = l ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
@@ -1490,16 +1490,16 @@ Lemma resize_all l x : resize (length l) x l = l.
 Proof. intros. by rewrite resize_le, take_ge. Qed.
 Lemma resize_all_alt l n x : n = length l → resize n x l = l.
 Proof. intros ->. by rewrite resize_all. Qed.
-Lemma resize_plus l n m x :
+Lemma resize_add l n m x :
   resize (n + m) x l = resize n x l ++ resize m x (drop n l).
 Proof.
   revert n m. induction l; intros [|?] [|?]; f_equal/=; auto.
   - by rewrite Nat.add_0_r, (right_id_L [] (++)).
-  - by rewrite replicate_plus.
+  - by rewrite replicate_add.
 Qed.
-Lemma resize_plus_eq l n m x :
+Lemma resize_add_eq l n m x :
   length l = n → resize (n + m) x l = l ++ replicate m x.
-Proof. intros <-. by rewrite resize_plus, resize_all, drop_all, resize_nil. Qed.
+Proof. intros <-. by rewrite resize_add, resize_all, drop_all, resize_nil. Qed.
 Lemma resize_app_le l1 l2 n x :
   n ≤ length l1 → resize n x (l1 ++ l2) = resize n x l1.
 Proof.
@@ -1537,7 +1537,7 @@ Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l.
 Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
 Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l.
 Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
-Lemma take_resize_plus l n m x : take n (resize (n + m) x l) = resize n x l.
+Lemma take_resize_add l n m x : take n (resize (n + m) x l) = resize n x l.
 Proof. by rewrite take_resize, min_l by lia. Qed.
 Lemma drop_resize_le l n m x :
   n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
@@ -1546,7 +1546,7 @@ Proof.
   - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
   - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
 Qed.
-Lemma drop_resize_plus l n m x :
+Lemma drop_resize_add l n m x :
   drop n (resize (n + m) x l) = resize m x (drop n l).
 Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
 Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
@@ -1578,7 +1578,7 @@ Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_old. Qed.
 Lemma rotate_replicate n1 n2 x:
   rotate n1 (replicate n2 x) = replicate n2 x.
 Proof.
-  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_plus.
+  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_add.
   f_equal. lia.
 Qed.
 
@@ -3355,7 +3355,7 @@ Section Forall2.
     { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
     intros. assert (n = length k); subst.
     { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
-    rewrite (nat_le_plus_minus (length k) m), !resize_plus,
+    rewrite (nat_le_add_sub (length k) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_r,
       Forall_resize, Forall_drop, resize_length.
@@ -3368,7 +3368,7 @@ Section Forall2.
     { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
     assert (n = length l); subst.
     { by rewrite (Forall2_length l (resize n y k)), resize_length. }
-    rewrite (nat_le_plus_minus (length l) m), !resize_plus,
+    rewrite (nat_le_add_sub (length l) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_l,
       Forall_resize, Forall_drop, resize_length.
@@ -3802,7 +3802,7 @@ Section find.
           naive_solver eauto using lookup_app_l_Some with lia. }
         apply list_find_Some. split_and!; [done..|].
         intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
-        by rewrite lookup_app_r, nat_minus_plus by lia.
+        by rewrite lookup_app_r, nat_sub_add by lia.
     - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
       + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
         assert (i < length l1) by eauto using lookup_lt_Some.
diff --git a/stdpp/nat_cancel.v b/stdpp/nat_cancel.v
index d0372a22a20fe297667b11cbfc008f3ede198dee..1fac15932f41d606c22e77d087d36d67cdd06232 100644
--- a/stdpp/nat_cancel.v
+++ b/stdpp/nat_cancel.v
@@ -64,22 +64,22 @@ Module nat_cancel.
   Global Instance make_nat_S_1 n : MakeNatS 1 n (S n).
   Proof. done. Qed.
 
-  Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
-  Global Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
+  Class MakeNatAdd (n1 n2 m : nat) := make_nat_add : m = n1 + n2.
+  Global Instance make_nat_add_0_l n : MakeNatAdd 0 n n.
   Proof. done. Qed.
-  Global Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
-  Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
-  Global Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
+  Global Instance make_nat_add_0_r n : MakeNatAdd n 0 n.
+  Proof. unfold MakeNatAdd. by rewrite Nat.add_0_r. Qed.
+  Global Instance make_nat_add_default n1 n2 : MakeNatAdd n1 n2 (n1 + n2) | 100.
   Proof. done. Qed.
 
   Global Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
   Proof. by unfold NatCancelR, NatCancelL. Qed.
   Global Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
   Proof. by unfold NatCancelR. Qed.
-  Global Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
+  Global Instance nat_cancel_leaf_add m m' m'' n1 n2 n1' n2' n1'n2' :
     NatCancelR m n1 m' n1' → NatCancelR m' n2 m'' n2' →
-    MakeNatPlus n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
-  Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. lia. Qed.
+    MakeNatAdd n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
+  Proof. unfold NatCancelR, NatCancelL, MakeNatAdd. lia. Qed.
   Global Instance nat_cancel_leaf_S_here m n m' n' :
     NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3.
   Proof. unfold NatCancelR, NatCancelL. lia. Qed.
@@ -92,10 +92,10 @@ Module nat_cancel.
   Global Instance nat_cancel_S_both m n m' n' :
     NatCancelL m n m' n' → NatCancelL (S m) (S n) m' n' | 1.
   Proof. unfold NatCancelL. lia. Qed.
-  Global Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
+  Global Instance nat_cancel_add m1 m2 m1' m2' m1'm2' n n' n'' :
     NatCancelL m1 n m1' n' → NatCancelL m2 n' m2' n'' →
-    MakeNatPlus m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
-  Proof. unfold NatCancelL, MakeNatPlus. lia. Qed.
+    MakeNatAdd m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
+  Proof. unfold NatCancelL, MakeNatAdd. lia. Qed.
   Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
     NatCancelL m n m' n' → NatCancelR 1 n' m'' n'' →
     MakeNatS m'' m' Sm' → NatCancelL (S m) n Sm' n'' | 3.
diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index 4f72314302e0bfea69cae39fd9fda484d4e258cc..91cec423558f9c89fe8bd6b6f86115de1915c051 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -11,7 +11,7 @@ Global Instance comparison_eq_dec : EqDecision comparison.
 Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
-Global Arguments minus !_ !_ / : assert.
+Global Arguments Nat.sub !_ !_ / : assert.
 Global Arguments Nat.max : simpl nomatch.
 
 Typeclasses Opaque lt.
@@ -66,10 +66,10 @@ Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
 Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
 
 (** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
-Lemma nat_minus_plus n m : n + m - n = m.
+Lemma nat_sub_add n m : n + m - n = m.
 Proof. lia. Qed.
 (** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
-Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n).
+Lemma nat_le_add_sub n m : n ≤ m → m = n + (m - n).
 Proof. lia. Qed.
 
 Lemma Nat_lt_succ_succ n : n < S (S n).
diff --git a/stdpp/relations.v b/stdpp/relations.v
index c09ae6b9c940961879d4f7a7cee513d3cb9a7a82..badc1c07d6483a8b091a69086800e2060b7af6a6 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -150,7 +150,7 @@ Section general.
   Lemma nsteps_r n x y z : nsteps R n x y → R y z → nsteps R (S n) x z.
   Proof. induction 1; eauto. Qed.
 
-  Lemma nsteps_plus_inv n m x z :
+  Lemma nsteps_add_inv n m x z :
     nsteps R (n + m) x z → ∃ y, nsteps R n x y ∧ nsteps R m y z.
   Proof.
     revert x.
@@ -161,7 +161,7 @@ Section general.
   Lemma nsteps_inv_r n x z : nsteps R (S n) x z → ∃ y, nsteps R n x y ∧ R y z.
   Proof.
     rewrite <- PeanoNat.Nat.add_1_r.
-    intros (?&?&?%nsteps_once_inv)%nsteps_plus_inv; eauto.
+    intros (?&?&?%nsteps_once_inv)%nsteps_add_inv; eauto.
   Qed.
 
   Lemma nsteps_congruence {B} (f : A → B) (R' : relation B) n x y :
@@ -171,22 +171,22 @@ Section general.
   (** ** Results about [bsteps] *)
   Lemma bsteps_once n x y : R x y → bsteps R (S n) x y.
   Proof. eauto. Qed.
-  Lemma bsteps_plus_r n m x y :
+  Lemma bsteps_add_r n m x y :
     bsteps R n x y → bsteps R (n + m) x y.
   Proof. induction 1; simpl; eauto. Qed.
   Lemma bsteps_weaken n m x y :
     n ≤ m → bsteps R n x y → bsteps R m x y.
   Proof.
-    intros. rewrite (nat_le_plus_minus n m); auto using bsteps_plus_r.
+    intros. rewrite (nat_le_add_sub n m); auto using bsteps_add_r.
   Qed.
-  Lemma bsteps_plus_l n m x y :
+  Lemma bsteps_add_l n m x y :
     bsteps R n x y → bsteps R (m + n) x y.
   Proof. apply bsteps_weaken. auto with arith. Qed.
   Lemma bsteps_S n x y :  bsteps R n x y → bsteps R (S n) x y.
   Proof. apply bsteps_weaken. lia. Qed.
   Lemma bsteps_trans n m x y z :
     bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
-  Proof. induction 1; simpl; eauto using bsteps_plus_l. Qed.
+  Proof. induction 1; simpl; eauto using bsteps_add_l. Qed.
   Lemma bsteps_r n x y z : bsteps R n x y → R y z → bsteps R (S n) x z.
   Proof. induction 1; eauto. Qed.
   Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 0e6dd8ae399f987088ab7af4c052bbac12889f0f..2e1e3a0687500cab80764a0a7a159cbb22a326e5 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -1265,17 +1265,17 @@ Section set_seq.
     - rewrite set_seq_subseteq; lia.
   Qed.
 
-  Lemma set_seq_plus_disjoint start len1 len2 :
+  Lemma set_seq_add_disjoint start len1 len2 :
     set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
   Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus start len1 len2 :
+  Lemma set_seq_add start len1 len2 :
     set_seq (C:=C) start (len1 + len2)
     ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
   Proof. set_solver by lia. Qed.
-  Lemma set_seq_plus_L `{!LeibnizEquiv C} start len1 len2 :
+  Lemma set_seq_add_L `{!LeibnizEquiv C} start len1 len2 :
     set_seq (C:=C) start (len1 + len2)
     = set_seq start len1 ∪ set_seq (start + len1) len2.
-  Proof. unfold_leibniz. apply set_seq_plus. Qed.
+  Proof. unfold_leibniz. apply set_seq_add. Qed.
 
   Lemma set_seq_S_start_disjoint start len :
     {[ start ]} ## set_seq (C:=C) (S start) len.