diff --git a/coq-iris.opam b/coq-iris.opam
index 5e3a91ef7875860abbe1274540645ca205631d7d..dfc8afa67a59223f926c66c4276e82793b7aa281 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-08-11.4.409da1f6") | (= "dev") }
+  "coq-stdpp" { (= "2022-08-12.3.d6c6e66a") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 3511d31b66bfeb7faedd0c87eb28329c80fa3cb4..0c8c16b93ab0f22b41169844180835c3ad7969db 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -103,7 +103,7 @@ Section dfrac.
 
   Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
   Proof.
-    rewrite Qp_lt_sum. split.
+    rewrite Qp.lt_sum. split.
     - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
     - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
   Qed.
@@ -120,18 +120,18 @@ Section dfrac.
     - intros [?| |?] [?| |?] [?| |?];
         rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
     - intros [?| |?] [?| |?];
-        rewrite /op /dfrac_op_instance 1?(comm_L Qp_add); done.
+        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
     - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
         rewrite /op /dfrac_op_instance; done.
     - intros [?| |?] ? [= <-]; done.
     - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
         apply dfrac_discarded_included.
     - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_le_add_l.
-      + apply Qp_lt_le_incl.
-      + intros. trans (q + q')%Qp; [|by apply Qp_lt_le_incl]. apply Qp_le_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
+      + apply Qp.lt_le_incl.
+      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
   Qed.
   Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
@@ -142,19 +142,19 @@ Section dfrac.
   Proof.
     intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
-    - apply Qp_not_add_le_l.
-    - move=> /Qp_lt_le_incl. apply Qp_not_add_le_l.
+    - apply Qp.not_add_le_l.
+    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
   Qed.
 
   Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
   Proof.
     apply: discrete_cancelable.
     intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
-    - by destruct (Qp_add_id_free q q2).
-    - by destruct (Qp_add_id_free q q1).
+    - by destruct (Qp.add_id_free q q2).
+    - by destruct (Qp.add_id_free q q1).
   Qed.
   Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
-  Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
+  Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
 
@@ -166,8 +166,8 @@ Section dfrac.
   Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
   Proof.
     destruct dq as [q'| |q']; [|done|].
-    - apply Qp_lt_le_trans, Qp_lt_add_r.
-    - intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
+    - apply Qp.lt_le_trans, Qp.lt_add_r.
+    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
   Qed.
 
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 0747d5a1e7a51d48afcf2d5795818f15c9f915f5..8072915ee1fbc21c1fde31d25816333e7a95a6bc 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -26,32 +26,32 @@ Section frac.
   Lemma frac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
-  Proof. by rewrite Qp_lt_sum. Qed.
+  Proof. by rewrite Qp.lt_sum. Qed.
 
   Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
-  Proof. rewrite frac_included. apply Qp_lt_le_incl. Qed.
+  Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.
 
   Definition frac_ra_mixin : RAMixin frac.
   Proof.
     split; try apply _; try done.
     intros p q. rewrite !frac_valid frac_op=> ?.
-    trans (p + q)%Qp; last done. apply Qp_le_add_l.
+    trans (p + q)%Qp; last done. apply Qp.le_add_l.
   Qed.
   Canonical Structure fracR := discreteR frac frac_ra_mixin.
 
   Global Instance frac_cmra_discrete : CmraDiscrete fracR.
   Proof. apply discrete_cmra_discrete. Qed.
   Global Instance frac_full_exclusive : Exclusive 1%Qp.
-  Proof. intros p. apply Qp_not_add_le_l. Qed.
+  Proof. intros p. apply Qp.not_add_le_l. Qed.
   Global Instance frac_cancelable (q : frac) : Cancelable q.
-  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
   Global Instance frac_id_free (q : frac) : IdFree q.
-  Proof. intros p _. apply Qp_add_id_free. Qed.
+  Proof. intros p _. apply Qp.add_id_free. Qed.
 
   (* This one has a higher precendence than [is_op_op] so we get a [+] instead
      of an [â‹…]. *)
   Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
   Proof. done. Qed.
   Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
 End frac.
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 751285832e74e5e957e0d1133c4cf28e0f655f61..7acc8c12560acc72aa448718b3e9c9fdacf611d0 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -9,7 +9,7 @@ Section nat.
   Local Instance nat_op_instance : Op nat := plus.
   Definition nat_op x y : x â‹… y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
-  Proof. by rewrite nat_le_sum. Qed.
+  Proof. by rewrite Nat.le_sum. Qed.
   Lemma nat_ra_mixin : RAMixin nat.
   Proof.
     apply ra_total_mixin; try by eauto.
@@ -165,7 +165,7 @@ Section positive.
   Local Instance pos_op_instance : Op positive := Pos.add.
   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.
+  Proof. by rewrite Pos.lt_sum. Qed.
   Lemma pos_ra_mixin : RAMixin positive.
   Proof.
     split; try by eauto.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index e74c5775832c4e0882af61d8f17a1c1263c89ad2..61c1f1717128c6a89a56c3097e7a1357e0bc38a9 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -398,7 +398,7 @@ Section fixpoint.
     { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
       induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
     rewrite -(fixpoint_unique fp2) //.
-    apply Hlim=> n /=. by apply Nat_iter_ind.
+    apply Hlim=> n /=. by apply Nat.iter_ind.
   Qed.
 End fixpoint.
 
@@ -440,7 +440,7 @@ Section fixpointK.
   Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f).
   Proof.
     symmetry. rewrite /fixpointK. apply fixpoint_unique.
-    by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
+    by rewrite -Nat.iter_succ_r Nat.iter_succ -fixpoint_unfold.
   Qed.
 
   Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f.
@@ -471,7 +471,7 @@ Section fixpointK.
     P (fixpointK k f).
   Proof.
     intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
-    intros; apply Nat_iter_ind; auto.
+    intros; apply Nat.iter_ind; auto.
   Qed.
 End fixpointK.
 
diff --git a/iris/algebra/ufrac.v b/iris/algebra/ufrac.v
index 66adffbcbb991d68538d07a29f3031f2e8b9cac5..e3ee45c72132d8287f1d0d2a233dbda99b431b58 100644
--- a/iris/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -21,10 +21,10 @@ Section ufrac.
   Lemma ufrac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma ufrac_included p q : p ≼ q ↔ (p < q)%Qp.
-  Proof. by rewrite Qp_lt_sum. Qed.
+  Proof. by rewrite Qp.lt_sum. Qed.
 
   Corollary ufrac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
-  Proof. rewrite ufrac_included. apply Qp_lt_le_incl. Qed.
+  Proof. rewrite ufrac_included. apply Qp.lt_le_incl. Qed.
 
   Definition ufrac_ra_mixin : RAMixin ufrac.
   Proof. split; try apply _; try done. Qed.
@@ -34,10 +34,10 @@ Section ufrac.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Global Instance ufrac_cancelable q : Cancelable q.
-  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
   Global Instance ufrac_id_free q : IdFree q.
-  Proof. intros p _. apply Qp_add_id_free. Qed.
+  Proof. intros p _. apply Qp.add_id_free. Qed.
 
   Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp.div_2. Qed.
 End ufrac.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 448b0d3f3c37bdb8de0c7598b0208ee540fd436a..56e720fd2352b23862c3d074917007f5fb42c20b 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -88,7 +88,7 @@ Section lemmas.
     ghost_var γ (1/2) a1 -∗
     ghost_var γ (1/2) a2 ==∗
     ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
-  Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
+  Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
 
   (** Framing support *)
   Global Instance frame_ghost_var p γ a q1 q2 RES :
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index fb2663030fd7f3de07ae5b1de3b398631f514e09..16babcffa4db27f2f66fd15a2db9a02cf5a256e1 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -67,7 +67,7 @@ Module gFunctors.
 
   Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
     GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
-              (fin_plus_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
+              (fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
 End gFunctors.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
@@ -99,8 +99,8 @@ Global Hint Mode subG ! + : typeclass_instances.
 Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
 Proof.
   move=> H; split.
-  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto.
-  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
+  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
+  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
 Qed.
 
 Global Instance subG_refl Σ : subG Σ Σ.
@@ -108,12 +108,12 @@ Proof. move=> i; by exists i. Qed.
 Global Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
-  exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
+  exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
 Qed.
 Global Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
-  exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
+  exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
 Qed.
 
 
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index de2dec96fa12a39b3472e477a1c178759920efa2..c54a4e46fe96b90271434143be6a085c7ef93c7d 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -92,7 +92,7 @@ Section later_credit_theory.
   Lemma lc_weaken {n} m :
     m ≤ n → £ n -∗ £ m.
   Proof.
-    intros [k ->]%nat_le_sum. rewrite lc_split. iIntros "[$ _]".
+    intros [k ->]%Nat.le_sum. rewrite lc_split. iIntros "[$ _]".
   Qed.
 
   Global Instance lc_timeless n : Timeless (£ n).
@@ -281,8 +281,8 @@ Module le_upd.
         + iModIntro. iDestruct "Hupd" as (m Hstep) "[Hown Hupd]". iNext.
           iPoseProof (IH with "Hown Hupd") as "Hit"; first done.
           clear IH.
-          assert (m ≤ n) as [k ->]%nat_le_sum by lia.
-          rewrite Nat.add_comm Nat_iter_add.
+          assert (m ≤ n) as [k ->]%Nat.le_sum by lia.
+          rewrite Nat.add_comm Nat.iter_add.
           iApply iter_modal_intro.
           { by iIntros (Q) "$". }
           iApply (iter_modal_mono with "[] Hit").
@@ -297,7 +297,7 @@ Module le_upd.
       Nat.iter (S n) (λ Q, |==> ▷ Q) P.
     Proof.
       iIntros "Hlc Hupd". iPoseProof (le_upd_elim with "Hlc Hupd") as "Hit".
-      rewrite Nat_iter_S_r. iApply (iter_modal_mono with "[] Hit").
+      rewrite Nat.iter_succ_r. iApply (iter_modal_mono with "[] Hit").
       { clear. iIntros (P Q) "Hent HP". by iApply "Hent". }
       iIntros "Hupd". iMod "Hupd". iModIntro. iMod "Hupd".
       iNext. iDestruct "Hupd" as "[%m (_ & _ & $)]".
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index a2515d89d0e787dfa98cb53600d6d05e2809e3fe..23bbf4a068978973ee4aab2a5482c7432b2bdf25 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -107,7 +107,7 @@ Section saved_anything.
     saved_anything_own γ (DfracOwn (1/2)) x1 -∗
     saved_anything_own γ (DfracOwn (1/2)) x2 ==∗
     saved_anything_own γ (DfracOwn (1/2)) y ∗ saved_anything_own γ (DfracOwn (1/2)) y.
-  Proof. iApply saved_anything_update_2. apply Qp_half_half. Qed.
+  Proof. iApply saved_anything_update_2. apply Qp.half_half. Qed.
 End saved_anything.
 
 (** Provide specialized versions of this for convenience. **)
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 935a206e703ec2755a4f4fcd92bb3b09efff620a..2303c1c3172aa0589a87cdba4a2eb919ee4e05cd 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -55,7 +55,7 @@ Section fractional.
   Lemma fractional_half P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P ⊣⊢ P12 ∗ P12.
-  Proof. by rewrite -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed.
+  Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->][-> _]. Qed.
   Lemma fractional_half_1 P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P -∗ P12 ∗ P12.
@@ -117,12 +117,12 @@ Section fractional.
   Global Instance mul_fractional_l Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_r. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_r. by apply H.
   Qed.
   Global Instance mul_fractional_r Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_l. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_l. by apply H.
   Qed.
 
   (* REMARK: These two instances do not work in either direction of the
@@ -156,11 +156,11 @@ Section fractional.
   Global Instance from_sep_fractional_half_fwd P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
     FromSep P Q Q | 10.
-  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
+  Proof. by rewrite /FromSep -{1}(Qp.div_2 q)=>-[-> ->] [-> _]. Qed.
   Global Instance from_sep_fractional_half_bwd P Q Φ q :
     AsFractional P Φ (q/2) → AsFractional Q Φ q →
     FromSep Q P P.
-  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
+  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp.div_2. Qed.
 
   Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -207,6 +207,6 @@ Section fractional.
     - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
     - rewrite fractional /Frame /MakeSep=><-<-=>_.
       by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
-    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
+    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp.div_2.
   Qed.
 End fractional.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index fdd9aa030ca8c39ce85194c5d49f174cd1acebcb..2db5890175d76bc160095c8495dfcea348b82fd4 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -520,7 +520,7 @@ Section fupd_derived.
   Lemma step_fupdN_S_fupd n E P :
     (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
-    apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
+    apply (anti_symm (⊢)); rewrite !Nat.iter_succ_r; apply step_fupdN_mono;
       rewrite -step_fupd_fupd //.
   Qed.
 
@@ -618,7 +618,7 @@ Section fupd_derived.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
-      - rewrite Nat_iter_S step_fupd_fupd IH !fupd_trans step_fupd_plain.
+      - rewrite Nat.iter_succ step_fupd_fupd IH !fupd_trans step_fupd_plain.
         apply fupd_mono. destruct n as [|n]; simpl.
         * by rewrite except_0_idemp.
         * by rewrite except_0_later.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index bf9cd4c33faa2bc8054d682983e4e54d52346a33..ae781fa791f05fce6e64f6b6ead3dd7191d73dbe 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -74,14 +74,14 @@ Proof.
   { inversion_clear 1; iIntros "? ? ?"; iExists 0=> /=.
     rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
   iIntros (Hsteps) "Hσ Hcred He". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite -(assoc_L (++)) Nat_iter_add -{1}plus_Sn_m plus_n_Sm.
+  rewrite -(assoc_L (++)) Nat.iter_add -{1}plus_Sn_m plus_n_Sm.
   rewrite lc_split. iDestruct "Hcred" as "[Hc1 Hc2]".
   iDestruct (wptp_step with "Hσ Hc1 He") as (nt') ">H"; first eauto; simplify_eq.
   iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
   iIntros ">(Hσ & He)". iMod (IH with "Hσ Hc2 He") as "IH"; first done. iModIntro.
   iApply (step_fupdN_wand with "IH"). iIntros ">IH".
   iDestruct "IH" as (nt'') "[??]".
-  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
+  rewrite -Nat.add_assoc -(assoc_L app) -replicate_add. by eauto with iFrame.
 Qed.
 
 Lemma wp_not_stuck κs nt e σ ns Φ :
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 61dc2888e47694f39922178dc0790a7197502736..40dbfa74e2089a722d5875b4dd78f487ee1a51f1 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -62,7 +62,7 @@ Section tada.
     iIntros (Φ) "_ HΦ".
     iMod (ghost_var_alloc Free) as (γvar) "Hvar".
     replace 1%Qp with (3/4 + 1/4)%Qp; last first.
-    { rewrite Qp_three_quarter_quarter //. }
+    { rewrite Qp.three_quarter_quarter //. }
     iDestruct "Hvar" as "[Hvar1 Hvar2]".
     wp_apply (l.(newlock_spec) with "Hvar2").
     iIntros (lk γlock) "Hlock".
@@ -82,7 +82,7 @@ Section tada.
     iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
     iDestruct (ghost_var_agree with "Hvar1 Hvar2") as %<-.
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
-    { rewrite Qp_quarter_three_quarter //. }
+    { rewrite Qp.quarter_three_quarter //. }
     iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"). done.
   Qed.
 
@@ -95,7 +95,7 @@ Section tada.
     iIntros "#Hislock %Φ AU". iApply fupd_wp.
     iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
     iMod (ghost_var_update_2 Free with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
-    { rewrite Qp_three_quarter_quarter //. }
+    { rewrite Qp.three_quarter_quarter //. }
     iMod ("Hclose" with "[$Hvar1]"). iModIntro.
     wp_apply (l.(release_spec) with "[$Hislock $Hlocked $Hvar2]").
     auto.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 506ac4cc71f5ec82f54c09325872fd89242f8e7b..0a74574194d1fc12b14ad50ab221e99e8ba05023 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -49,7 +49,7 @@ Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
 Lemma pending_split γ q :
   own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
 Proof.
-  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp_div_2 //.
+  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp.div_2 //.
 Qed.
 
 Lemma pending_shoot γ n :