diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index fbcaeea7a3f1caa104d8b0e51f1efdeab45c2bae..7dd05040b4c82781a650a0d43ec1cfbba6894027 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -70,11 +70,13 @@ Definition arcUR :=
          (prodUR (prodUR move_selfUR move_otherUR) move_otherUR).
 
 Class arcG Σ := {
-  ArcStG :> inG Σ arcUR;
-  ArcPrt_gpsG :> gpsG Σ unitProtocol;
-  Arc_atomG :> atomicG Σ;
-  Arc_viewInv :> view_invG Σ;
+  ArcStG : inG Σ arcUR;
+  ArcPrt_gpsG : gpsG Σ unitProtocol;
+  Arc_atomG : atomicG Σ;
+  Arc_viewInvG : view_invG Σ;
 }.
+#[global] Existing Instances ArcStG ArcPrt_gpsG Arc_atomG Arc_viewInvG.
+
 Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol; atomicΣ; view_invΣ].
 Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 3c7e5e4939b9cf7f3f2f96d9547aeb3086d043a2..bd99ed71eee173514d1d7050ded4bcb623a855c6 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -17,9 +17,10 @@ Definition acquire : val :=
 Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false.
 
 Class lockG Σ := LockG {
-  lock_gpsG :> gpsG Σ unitProtocol;
-  lock_atomG :> atomicG Σ;
+  lock_gpsG : gpsG Σ unitProtocol;
+  lock_atomG : atomicG Σ;
 }.
+#[global] Existing Instances lock_gpsG lock_atomG.
 
 Definition lockΣ : gFunctors := #[gpsΣ unitProtocol; atomicΣ].
 
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 0f57c0f21d1b170dda061400671d3b8843cef5d7..d6411671cd1b72c21085584075bdc528c2393abf 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -28,8 +28,9 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 Class spawnG Σ := SpawnG {
-  spawn_atomG :> atomicG Σ;
-  spawn_viewG :> view_invG Σ }.
+  spawn_atomG : atomicG Σ;
+  spawn_viewG : view_invG Σ }.
+#[global] Existing Instances spawn_atomG spawn_viewG.
 
 Definition spawnΣ : gFunctors := #[atomicΣ; view_invΣ].
 
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 0853bfd882f72024dcf37b2b86566c50a807904c..795a764b45e1ff31332f3ba1e8b8306e58d6704d 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -4,7 +4,8 @@ From iris.algebra Require Import frac.
 From lrust.lifetime Require Export lifetime.
 From iris.prelude Require Import options.
 
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG : inG Σ fracR.
+#[global] Existing Instance frac_borG_inG.
 
 Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}
                               (φ : Qp → monPred _ _) (V0 : Lat ) γ κ : monPred _ _:=
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 36117c724d3eb2ff47ffb0acf2e1c088159aff09..9ec10bc735553eb1303785dbd1625b8d41f3d0c9 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -8,8 +8,9 @@ From iris.prelude Require Import options.
 [gname]) to a lifetime (as is required for types using branding). *)
 
 Class lft_metaG Σ := LftMetaG {
-  lft_meta_inG :> inG Σ (dyn_reservation_mapR (agreeR gnameO));
+  lft_meta_inG : inG Σ (dyn_reservation_mapR (agreeR gnameO));
 }.
+#[global] Existing Instance lft_meta_inG.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
 Global Instance subG_lft_meta Σ :
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 7b9d0c8878dc8df31fbb2c331a1ab2d7457b6b25..0d9ceae9cda34ddcaf93518a8b3df0f72c5808af 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -11,9 +11,10 @@ Implicit Types Lat : latticeT.
 
 (** The CMRAs we need. *)
 Class boxG Lat Σ :=
-  boxG_inG :> inG Σ (prodR
+  boxG_inG : inG Σ (prodR
     (excl_authR (optionO (latO Lat)))
     (optionR (agreeR (laterO (Lat -d> iPropO Σ))))).
+#[local] Existing Instance boxG_inG.
 
 Definition boxΣ Lat : gFunctors := #[
    GFunctor (excl_authR (optionO (latO Lat)) *
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index d784b0db397897fac9a862fa3dd194b95a20f233..5b8dc144f4278a2f3e044934b0803cafe0b130a1 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -44,26 +44,31 @@ Definition borUR Lat := gmapUR slice_name (exclR (bor_stateO Lat)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftG Σ Lat (userE : coPset) := LftG {
-  lft_box :> boxG Lat Σ;
-  alft_inG :> inG Σ (authR (alftUR Lat));
+  lft_box : boxG Lat Σ;
+  alft_inG : inG Σ (authR (alftUR Lat));
   alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_inG : inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR (borUR Lat));
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
+  lft_bor_inG : inG Σ (authR (borUR Lat));
+  lft_cnt_inG : inG Σ (authR natUR);
+  lft_inh_inG : inG Σ (authR inhUR);
   userE_lftN_disj : ↑lftN ## userE;
 }.
+#[global] Existing Instances
+  lft_box alft_inG ilft_inG lft_bor_inG lft_cnt_inG lft_inh_inG.
 Definition lftG' := lftG.
 
 Class lftPreG Σ Lat := LftPreG {
-  lft_preG_box :> boxG Lat Σ;
-  alft_preG_inG :> inG Σ (authR (alftUR Lat));
-  ilft_preG_inG :> inG Σ (authR ilftUR);
-  lft_preG_bor_inG :> inG Σ (authR (borUR Lat));
-  lft_preG_cnt_inG :> inG Σ (authR natUR);
-  lft_preG_inh_inG :> inG Σ (authR inhUR);
+  lft_preG_box : boxG Lat Σ;
+  alft_preG_inG : inG Σ (authR (alftUR Lat));
+  ilft_preG_inG : inG Σ (authR ilftUR);
+  lft_preG_bor_inG : inG Σ (authR (borUR Lat));
+  lft_preG_cnt_inG : inG Σ (authR natUR);
+  lft_preG_inh_inG : inG Σ (authR inhUR);
 }.
+#[global] Existing Instances
+  lft_preG_box alft_preG_inG ilft_preG_inG
+  lft_preG_bor_inG lft_preG_cnt_inG lft_preG_inh_inG.
 Definition lftPreG' := lftPreG.
 
 Definition lftΣ Lat : gFunctors :=
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 71b899d2eb77e03626c9bcd9be4aeba380de3cab..539b417f22342ac3002a916f5b24a6480a1d1c8f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -876,13 +876,13 @@ Section arc.
       iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
       wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
+      iDestruct (ty_size_eq with "Hown") as %?. rewrite Nat.max_0_r.
       iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [auto..|].
       iIntros "[? Hrc']". wp_seq.
       wp_apply (drop_fake_spec with "[//] [$Hdrop Hrc' H†] "); [solve_ndisj|..].
       { unfold P2. auto with iFrame. } unlock. iIntros ([]); last first.
       { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
-        iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
+        iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Nat.max_0_r.
         auto 10 with iFrame. }
       iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
       iDestruct "Heq" as %<-. wp_if.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 819648eb82ea375c91a533de5031ed4b9449af71..4c7d6a163b68087f2570e102bd74c1cfce786d31 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -8,9 +8,10 @@ From iris.prelude Require Import options.
 
 Definition brandidx_stR := max_natUR.
 Class brandidxG Σ := BrandedIdxG {
-  brandidx_inG :> inG Σ (authR brandidx_stR);
-  brandidx_gsingletonG :> lft_metaG Σ;
+  brandidx_inG : inG Σ (authR brandidx_stR);
+  brandidx_gsingletonG : lft_metaG Σ;
 }.
+#[global] Existing Instances brandidx_inG brandidx_gsingletonG.
 
 Definition brandidxΣ : gFunctors
   := #[GFunctor (authR brandidx_stR); lft_metaΣ].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 61efc9bbe9c2493048fac990951533fc6516128a..4eb224d632f5bece72bfc2773bdda776679b6656 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -8,7 +8,8 @@ From iris.prelude Require Import options.
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
-  RcG :> inG Σ (authR rc_stR).
+  RcG : inG Σ (authR rc_stR).
+#[global] Existing Instance RcG.
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
 Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 82bc28756a1549c4f80e0b0e201f6557843a1820..5bc0bc919402befa28ef1a42584f378f850d4fd8 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -10,7 +10,8 @@ Definition refcell_stR :=
              fracR)
              positiveR).
 Class refcellG Σ :=
-  RefCellG :> inG Σ (authR refcell_stR).
+  RefCellG : inG Σ (authR refcell_stR).
+#[global] Existing Instance RefCellG.
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
 Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 0e67e0706e9004650f7572f1d9458b73521f645f..c05cf674668a5b4de71763b9ba7881a039978e34 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -13,10 +13,11 @@ Definition rwlock_stR :=
   optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Definition rwlockR := authR rwlock_stR.
 Class rwlockG Σ := RwLockG {
-  rwlock_stateG :> inG Σ rwlockR ;
-  rwlock_gpsG :> gpsG Σ unitProtocol;
-  rwlock_atomG :> atomicG Σ;
+  rwlock_stateG : inG Σ rwlockR ;
+  rwlock_gpsG : gpsG Σ unitProtocol;
+  rwlock_atomG : atomicG Σ;
 }.
+#[global] Existing Instances rwlock_stateG rwlock_gpsG rwlock_atomG.
 
 Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol; atomicΣ].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 11d525b0d1888b4a8e8d175fd0c8bc4df9a1b014..976583fadb7ff1e7cc87efc043798bcf49ce0459 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -115,7 +115,7 @@ Section product.
     iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first solve_ndisj.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. lia. }
     iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
-    { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
+    { move: HF. rewrite /= -Nat.add_assoc shr_locsE_shift.
       assert (shr_locsE l (ty_size ty1) ## shr_locsE (l +â‚— (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
       set_solver. }
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ad28872239c028d9cf3cb28792fdcf13800c631b..d016750175831999cf41a5658a7eb3cdfe1d1fbf 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -75,7 +75,7 @@ Section product_split.
       by iApply "Heq". }
     iMod ("IH" with "[] HL [Htyl]") as "(HL & Htyl)"; first done.
     { change (ty_size ty) with (0+ty_size ty)%nat at 1.
-      rewrite plus_comm -hasty_ptr_offsets_offset //. }
+      rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
     iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
                    last by rewrite tctx_interp_singleton.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 5cd4307df385d444627417e6b73d440689d45124..5f77054ec0c121a0f2348b631f43a7628cc19a38 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,11 +8,13 @@ From lrust.typing Require Import typing.
 From iris.prelude Require Import options.
 
 Class typePreG Σ := PreTypeG {
-  type_preG_heapG :> noprolGpreS Σ;
-  type_preG_lftG :> lftPreG Σ view_Lat;
-  type_preG_na_invG :> na_invG view_Lat Σ;
-  type_preG_frac_borG :> frac_borG Σ
+  type_preG_heapG : noprolGpreS Σ;
+  type_preG_lftG : lftPreG Σ view_Lat;
+  type_preG_na_invG : na_invG view_Lat Σ;
+  type_preG_frac_borG : frac_borG Σ
 }.
+#[global] Existing Instances
+  type_preG_heapG type_preG_lftG type_preG_na_invG type_preG_frac_borG.
 
 Definition typeΣ : gFunctors :=
   #[noprolΣ; lftΣ view_Lat; na_invΣ view_Lat; GFunctor (constRF fracR)].
diff --git a/theories/typing/type.v b/theories/typing/type.v
index fa26d247621806010f27715be9a6e1b0747d347f..ae9b7185a52c0411c748f53e9bb8c5687e2386ee 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -8,11 +8,12 @@ From lrust.typing Require Import lft_contexts.
 From iris.prelude Require Import options.
 
 Class typeG Σ := TypeG {
-  type_noprolG :> noprolG Σ;
-  type_lftG :> lftG Σ view_Lat lft_userE;
-  type_na_invG :> na_invG view_Lat Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_noprolG : noprolG Σ;
+  type_lftG : lftG Σ view_Lat lft_userE;
+  type_na_invG : na_invG view_Lat Σ;
+  type_frac_borrowG : frac_borG Σ
 }.
+#[global] Existing Instances type_noprolG type_lftG type_na_invG type_frac_borrowG.
 
 Definition lrustN := nroot .@ "lrust".
 Definition shrN  := lrustN .@ "shr".
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2a8eaeb8abd5a3195e9e06233b66a9df6755f75e..55098ec965f9d3b610b839e652f4e4983363885f 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -38,7 +38,7 @@ Section case.
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. auto.
       + eauto with iFrame.
-      + rewrite -EQlen app_length minus_plus shift_loc_assoc Nat2Z.id.
+      + rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
         iFrame. iExists _. iFrame. auto.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index d9c7adf15d84c60860184b22d2c5658c52350f8f..d61278e9d48db8f3eb47fc6f2e82bcbeea97aebf 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -84,7 +84,7 @@ Section uninit.
     subtype E L (uninit n) (Π(ty :: tyl)).
   Proof.
     intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
-    rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
+    rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm // replicate_add
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
   Lemma uninit_product_subtype_cons_l {E L} (n : nat) ty tyl :
@@ -94,7 +94,7 @@ Section uninit.
     subtype E L (Π(ty :: tyl)) (uninit n).
   Proof.
     intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
-    rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
+    rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm replicate_add
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
   Lemma uninit_product_eqtype_cons_r {E L} (n : nat) ty tyl :