diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index b0f38ffbf7814864f9dc6356c523a4750b417882..f35690e2a85d299582249411d04a392254cce765 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -185,10 +185,10 @@ Section list.
   Proof. intros f f' Hf l ? <-. apply big_opL_proper; intros; apply Hf. Qed.
 
   Lemma big_opL_consZ_l (f : Z → A → M) x l :
-    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (1 + k)%Z y.
+    ([^o list] k↦y ∈ x :: l, f (Z.of_nat k) y) = f 0%Z x `o` [^o list] k↦y ∈ l, f (1 + Z.of_nat k)%Z y.
   Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
   Lemma big_opL_consZ_r (f : Z → A → M) x l :
-    ([^o list] k↦y ∈ x :: l, f k y) = f 0 x `o` [^o list] k↦y ∈ l, f (k + 1)%Z y.
+    ([^o list] k↦y ∈ x :: l, f (Z.of_nat k) y) = f 0%Z x `o` [^o list] k↦y ∈ l, f (Z.of_nat k + 1)%Z y.
   Proof. rewrite big_opL_cons. auto using big_opL_ext with f_equal lia. Qed.
 
   Lemma big_opL_fmap {B} (h : A → B) (f : nat → B → M) l :
diff --git a/iris/prelude/prelude.v b/iris/prelude/prelude.v
index 936e9523e17ccf12af26e5eb15ba90e229d37f18..d915dfc3f165e0055c1527430ba5a928465a5b8b 100644
--- a/iris/prelude/prelude.v
+++ b/iris/prelude/prelude.v
@@ -4,6 +4,3 @@ From iris.prelude Require Import options.
 Global Open Scope general_if_scope.
 Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
 Ltac done := stdpp.tactics.done.
-
-(** Iris itself and many dependencies still rely on this coercion. *)
-Coercion Z.of_nat : nat >-> Z.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index e4e218a72904737906c412e52394756f4d73d448..128627e3d2c06371ccca0e44da674cb15e960054 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -15,7 +15,7 @@ From iris.prelude Require Import options.
 with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
-  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ Z.of_nat i) ↦{dq} v)%I.
 
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
 has been fixed. *)
@@ -56,7 +56,7 @@ Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
 Lemma array_app l dq vs ws :
-  l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
+  l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ Z.of_nat (length vs)) ↦∗{dq} ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
@@ -78,7 +78,9 @@ Proof. by rewrite /Frame array_cons. Qed.
 
 Lemma update_array l dq vs off v :
   vs !! off = Some v →
-  ⊢ l ↦∗{dq} vs -∗ ((l +ₗ off) ↦{dq} v ∗ ∀ v', (l +ₗ off) ↦{dq} v' -∗ l ↦∗{dq} <[off:=v']>vs).
+  l ↦∗{dq} vs -∗
+  ((l +ₗ Z.of_nat off) ↦{dq} v ∗
+    ∀ v', (l +ₗ Z.of_nat off) ↦{dq} v' -∗ l ↦∗{dq} <[off:=v']>vs).
 Proof.
   iIntros (Hlookup) "Hl".
   rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
@@ -97,7 +99,7 @@ Qed.
 
 (** * Rules for allocation *)
 Lemma mapsto_seq_array l dq v n :
-  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
+  ([∗ list] i ∈ seq 0 n, (l +ₗ (Z.of_nat i)) ↦{dq} v) -∗
   l ↦∗{dq} replicate n v.
 Proof.
   rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
@@ -111,7 +113,7 @@ Lemma twp_allocN s E v n :
   (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (Z.of_nat i)) ⊤ }]].
 Proof.
   iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
   iIntros (l) "Hlm". iApply "HΦ".
@@ -122,7 +124,7 @@ Lemma wp_allocN s E v n :
   (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (Z.of_nat i)) ⊤ }}}.
 Proof.
   iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
   iApply twp_allocN; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
@@ -133,7 +135,7 @@ Lemma twp_allocN_vec s E v n :
   [[{ True }]]
     AllocN #n v @ s ; E
   [[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (Z.of_nat i)) ⊤ }]].
 Proof.
   iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN; [ lia | done | .. ].
   iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
@@ -143,7 +145,7 @@ Lemma wp_allocN_vec s E v n :
   {{{ True }}}
     AllocN #n v @ s ; E
   {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
-         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (Z.of_nat i)) ⊤ }}}.
 Proof.
   iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
   iApply twp_allocN_vec; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
@@ -152,7 +154,7 @@ Qed.
 (** * Rules for accessing array elements *)
 Lemma twp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ Z.of_nat off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -162,22 +164,22 @@ Proof.
 Qed.
 Lemma wp_load_offset s E l dq off vs v :
   vs !! off = Some v →
-  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ Z.of_nat off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
-  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
+  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ Z.of_nat off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
 Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
 Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
+  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ Z.of_nat off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
 
 Lemma twp_store_offset s E l off vs v :
   is_Some (vs !! off) →
-  [[{ l ↦∗ vs }]] #(l +ₗ off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
+  [[{ l ↦∗ vs }]] #(l +ₗ Z.of_nat off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
 Proof.
   iIntros ([w Hlookup] Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -186,20 +188,20 @@ Proof.
 Qed.
 Lemma wp_store_offset s E l off vs v :
   is_Some (vs !! off) →
-  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ Z.of_nat off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_store_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-  [[{ l ↦∗ vs }]] #(l +ₗ off) <- v @ s; E [[{ RET #(); l ↦∗ vinsert off v vs }]].
+  [[{ l ↦∗ vs }]] #(l +ₗ Z.of_nat off) <- v @ s; E [[{ RET #(); l ↦∗ vinsert off v vs }]].
 Proof.
   setoid_rewrite vec_to_list_insert. apply twp_store_offset.
   eexists. by apply vlookup_lookup.
 Qed.
 Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
+  {{{ ▷ l ↦∗ vs }}} #(l +ₗ Z.of_nat off) <- v @ s; E {{{ RET #(); l ↦∗ vinsert off v vs }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_store_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
@@ -207,7 +209,7 @@ Qed.
 
 Lemma twp_xchg_offset s E l off vs v v' :
   vs !! off = Some v →
-  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ Z.of_nat off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
 Proof.
   iIntros (Hlookup Φ) "Hl HΦ".
   iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
@@ -216,20 +218,20 @@ Proof.
 Qed.
 Lemma wp_xchg_offset s E l off vs v v' :
   vs !! off = Some v →
-  {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
+  {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ Z.of_nat off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_xchg_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
 
 Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
+  [[{ l ↦∗ vs }]] Xchg #(l +ₗ Z.of_nat off) v @ s; E [[{ RET (vs !!! off); l ↦∗ vinsert off v vs }]].
 Proof.
   setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
   by apply vlookup_lookup.
 Qed.
 Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
-   {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
+   {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ Z.of_nat off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
 Proof.
   iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_xchg_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
@@ -240,7 +242,7 @@ Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   v' = v1 →
   vals_compare_safe v' v1 →
   [[{ l ↦∗ vs }]]
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   [[{ RET (v', #true); l ↦∗ <[off:=v2]> vs }]].
 Proof.
   iIntros (Hlookup ?? Φ) "Hl HΦ".
@@ -253,7 +255,7 @@ Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
   v' = v1 →
   vals_compare_safe v' v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
 Proof.
   iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
@@ -264,7 +266,7 @@ Lemma twp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2
   vs !!! off = v1 →
   vals_compare_safe (vs !!! off) v1 →
   [[{ l ↦∗ vs }]]
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   [[{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }]].
 Proof.
   intros. setoid_rewrite vec_to_list_insert. eapply twp_cmpxchg_suc_offset=> //.
@@ -274,7 +276,7 @@ Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2
   vs !!! off = v1 →
   vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   {{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
 Proof.
   iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
@@ -286,7 +288,7 @@ Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
   [[{ l ↦∗{dq} vs }]]
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   [[{ RET (v0, #false); l ↦∗{dq} vs }]].
 Proof.
   iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
@@ -301,7 +303,7 @@ Lemma wp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
   v0 ≠ v1 →
   vals_compare_safe v0 v1 →
   {{{ ▷ l ↦∗{dq} vs }}}
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   {{{ RET (v0, #false); l ↦∗{dq} vs }}}.
 Proof.
   iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
@@ -312,20 +314,20 @@ Lemma twp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
   [[{ l ↦∗{dq} vs }]]
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   [[{ RET (vs !!! off, #false); l ↦∗{dq} vs }]].
 Proof. intros. eapply twp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 Lemma wp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
   vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗{dq} vs }}}
-    CmpXchg #(l +â‚— off) v1 v2 @ s; E
+    CmpXchg #(l +â‚— Z.of_nat off) v1 v2 @ s; E
   {{{ RET (vs !!! off, #false); l ↦∗{dq} vs }}}.
 Proof. intros. eapply wp_cmpxchg_fail_offset=> //. by apply vlookup_lookup. Qed.
 
 Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
   vs !! off = Some #i1 →
-  [[{ l ↦∗ vs }]] FAA #(l +ₗ off) #i2 @ s; E
+  [[{ l ↦∗ vs }]] FAA #(l +ₗ Z.of_nat off) #i2 @ s; E
   [[{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }]].
 Proof.
   iIntros (Hlookup Φ) "Hl HΦ".
@@ -335,7 +337,7 @@ Proof.
 Qed.
 Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
   vs !! off = Some #i1 →
-  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
+  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ Z.of_nat off) #i2 @ s; E
   {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
@@ -344,7 +346,7 @@ Qed.
 
 Lemma twp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
   vs !!! off = #i1 →
-  [[{ l ↦∗ vs }]] FAA #(l +ₗ off) #i2 @ s; E
+  [[{ l ↦∗ vs }]] FAA #(l +ₗ Z.of_nat off) #i2 @ s; E
   [[{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }]].
 Proof.
   intros. setoid_rewrite vec_to_list_insert. apply twp_faa_offset=> //.
@@ -352,7 +354,7 @@ Proof.
 Qed.
 Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
   vs !!! off = #i1 →
-  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
+  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ Z.of_nat off) #i2 @ s; E
   {{{ RET LitV (LitInt i1); l ↦∗ vinsert off #(i1 + i2) vs }}}.
 Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index f435cb81c792230cadb7fe30e5e8013bb590bcdc..58240c1207fef3dd0648f84f644a047e7c6b63db 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -595,9 +595,9 @@ Proof.
   { rewrite lookup_empty. naive_solver lia. }
   rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
   - intros [[-> ?] | (Hl & j & w & ? & -> & -> & ?)].
-    { eexists 0, _. rewrite loc_add_0. naive_solver lia. }
+    { eexists 0%Z, _. rewrite loc_add_0. naive_solver lia. }
     eexists (1 + j)%Z, _. rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
-  - intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
+  - intros (j & w & ? & -> & -> & Hil). destruct (decide (j = 0%Z)); simplify_eq/=.
     { rewrite loc_add_0; eauto. }
     right. split.
     { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
@@ -609,7 +609,7 @@ Proof.
 Qed.
 
 Lemma heap_array_map_disjoint (h : gmap loc (option val)) (l : loc) (vs : list val) :
-  (∀ i, (0 ≤ i)%Z → (i < length vs)%Z → h !! (l +ₗ i) = None) →
+  (∀ i, (0 ≤ i)%Z → (i < Z.of_nat (length vs))%Z → h !! (l +ₗ i) = None) →
   (heap_array l vs) ##ₘ h.
 Proof.
   intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
diff --git a/iris_heap_lang/lib/arith.v b/iris_heap_lang/lib/arith.v
index 8a2165ce6becbac4b2e21575bfa4ef66d3abcd62..24e69ec9bdfd73b1d8eaa7bfe1181a906bfe7bb0 100644
--- a/iris_heap_lang/lib/arith.v
+++ b/iris_heap_lang/lib/arith.v
@@ -26,7 +26,7 @@ Qed.
 Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
   ▷ Φ #(m `min` n)%nat -∗
   WP minimum #m #n @ s;E {{ Φ }}.
-Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
+Proof. iIntros "HΦ". iApply minimum_spec. by rewrite /LitNat Nat2Z.inj_min. Qed.
 
 Lemma maximum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
   ▷ Φ #(m `max` n) -∗
@@ -40,4 +40,4 @@ Qed.
 Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
   ▷ Φ #(m `max` n)%nat -∗
   WP maximum #m #n @ s;E {{ Φ }}.
-Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
+Proof. iIntros "HΦ". iApply maximum_spec. by rewrite /LitNat Nat2Z.inj_max. Qed.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 86598a764c749236289e61dc46eb0341aa83c35e..d4b55f5161404ffa035f19397de0ce65f01165c5 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -53,7 +53,7 @@ Section proof.
   Context `{!heapG Σ}.
 
   Lemma twp_array_free s E l vs (n : Z) :
-    n = length vs →
+    n = Z.of_nat (length vs) →
     [[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
   Proof.
     iIntros (Hlen Φ) "Hl HΦ".
@@ -63,7 +63,7 @@ Section proof.
     wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
   Qed.
   Lemma wp_array_free s E l vs (n : Z) :
-    n = length vs →
+    n = Z.of_nat (length vs) →
     {{{ l ↦∗ vs }}} array_free #l #n @ s; E {{{ RET #(); True }}}.
   Proof.
     iIntros (? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
@@ -132,12 +132,12 @@ Section proof.
     Local Lemma wp_array_init_loop stk E l i n k f  :
       n = Z.of_nat (i + k) →
       {{{
-        (l +ₗ i) ↦∗ replicate k #() ∗
-        [∗ list] j ∈ seq i k, WP f #(j : nat) @ stk; E {{ Q j }}
+        (l +ₗ Z.of_nat i) ↦∗ replicate k #() ∗
+        [∗ list] j ∈ seq i k, WP f #(Z.of_nat j) @ stk; E {{ Q j }}
       }}}
-        array_init_loop #l #i #n f @ stk; E
+        array_init_loop #l #(Z.of_nat i) #n f @ stk; E
       {{{ vs, RET #();
-        ⌜ length vs = k ⌝ ∗ (l +ₗ i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
+        ⌜ length vs = k ⌝ ∗ (l +ₗ Z.of_nat i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
       }}}.
     Proof.
       iIntros (Hn Φ) "[Hl Hf] HΦ".
@@ -159,12 +159,12 @@ Section proof.
     Local Lemma twp_array_init_loop stk E l i n k f  :
       n = Z.of_nat (i + k) →
       [[{
-        (l +ₗ i) ↦∗ replicate k #() ∗
-        [∗ list] j ∈ seq i k, WP f #(j : nat) @ stk; E [{ Q j }]
+        (l +ₗ Z.of_nat i) ↦∗ replicate k #() ∗
+        [∗ list] j ∈ seq i k, WP f #(Z.of_nat j) @ stk; E [{ Q j }]
       }]]
-        array_init_loop #l #i #n f @ stk; E
+        array_init_loop #l #(Z.of_nat i) #n f @ stk; E
       [[{ vs, RET #();
-        ⌜ length vs = k ⌝ ∗ (l +ₗ i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
+        ⌜ length vs = k ⌝ ∗ (l +ₗ Z.of_nat i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
       }]].
     Proof.
       iIntros (Hn Φ) "[Hl Hf] HΦ".
@@ -187,7 +187,7 @@ Section proof.
     Lemma wp_array_init stk E n f :
       (0 < n)%Z →
       {{{
-        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E {{ Q i }}
+        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(Z.of_nat i) @ stk; E {{ Q i }}
       }}}
         array_init #n f @ stk; E
       {{{ l vs, RET #l;
@@ -206,7 +206,7 @@ Section proof.
     Lemma twp_array_init stk E n f :
       (0 < n)%Z →
       [[{
-        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E [{ Q i }]
+        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(Z.of_nat i) @ stk; E [{ Q i }]
       }]]
         array_init #n f @ stk; E
       [[{ l vs, RET #l;
@@ -243,7 +243,7 @@ Section proof.
       (0 < n)%Z →
       {{{
         [∗ list] i ∈ seq 0 (Z.to_nat n),
-          WP f #(i : nat) @ stk; E {{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }}
+          WP f #(Z.of_nat i) @ stk; E {{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }}
       }}}
         array_init #n f @ stk; E
       {{{ l xs, RET #l;
@@ -259,7 +259,7 @@ Section proof.
       (0 < n)%Z →
       [[{
         [∗ list] i ∈ seq 0 (Z.to_nat n),
-          WP f #(i : nat) @ stk; E [{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }]
+          WP f #(Z.of_nat i) @ stk; E [{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }]
       }]]
         array_init #n f @ stk; E
       [[{ l xs, RET #l;
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index c4a4a0357adb56472bd36215ab8d4ce9963036ec..2c849d51ff9742d6942d939fd17abec0fec50834 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -58,7 +58,7 @@ Section mono_proof.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+      { iNext. iExists (S c). rewrite /LitNat Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. iApply "HΦ". iModIntro. iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
@@ -135,7 +135,7 @@ Section contrib_spec.
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+      { iNext. iExists (S c). rewrite /LitNat Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. by iApply "HΦ".
     - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
       iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index a36221a3a58b05d003fa2e563871a48d0bb73256..0b312ff7a7a979d6bcc03a84ad098710c0007c89 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -131,7 +131,7 @@ Section proof.
       rewrite -(set_seq_S_end_union_L 0).
       wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
-        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
+        rewrite /LitNat Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       wp_pures.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
@@ -166,7 +166,7 @@ Section proof.
       by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
     iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
     iIntros "!> !>". iExists (S o), n'.
-    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
+    rewrite /LitNat Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
   Qed.
 End proof.
 
diff --git a/iris_heap_lang/notation.v b/iris_heap_lang/notation.v
index 6ea7e8eaab90a9a81d1d5ca063b227d732ceafbf..29c667afd9097db0fb259d235e51efcd8116fb8e 100644
--- a/iris_heap_lang/notation.v
+++ b/iris_heap_lang/notation.v
@@ -7,6 +7,7 @@ Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
 Coercion LitProphecy : proph_id >-> base_lit.
+Coercion LitNat (n : nat) : base_lit := LitInt (Z.of_nat n).
 
 Coercion App : expr >-> Funclass.
 
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 87adf2a6b1a1d6aa7c4207e46c95fce3d18b4b59..022410f00677b40093cbf605823b237282bb6d93 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -188,7 +188,7 @@ are derived in te file [array]. *)
 Lemma heap_array_to_seq_meta l vs (n : nat) :
   length vs = n →
   ([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l' ⊤) -∗
-  [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)) ⊤.
+  [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (Z.of_nat i)) ⊤.
 Proof.
   iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
   rewrite big_opM_union; last first.
@@ -203,7 +203,7 @@ Qed.
 
 Lemma heap_array_to_seq_mapsto l v (n : nat) :
   ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -∗
-  [∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
+  [∗ list] i ∈ seq 0 n, (l +ₗ (Z.of_nat i)) ↦ v.
 Proof.
   iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
   { done. }
@@ -221,7 +221,7 @@ Lemma twp_allocN_seq s E v n :
   (0 < n)%Z →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
-      (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }]].
+      (l +ₗ (Z.of_nat i)) ↦ v ∗ meta_token (l +ₗ (Z.of_nat i)) ⊤ }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
@@ -239,7 +239,7 @@ Lemma wp_allocN_seq s E v n :
   (0 < n)%Z →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
   {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 (Z.to_nat n),
-      (l +ₗ (i : nat)) ↦ v ∗ meta_token (l +ₗ (i : nat)) ⊤ }}}.
+      (l +ₗ (Z.of_nat i)) ↦ v ∗ meta_token (l +ₗ (Z.of_nat i)) ⊤ }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
   iApply twp_allocN_seq; [by auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index 8d7e31a97105ed57ba50d9fdef6034f27d46a8b9..32e62be7145daffd3cac2606b76c6c9d19a9d624 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -512,7 +512,7 @@ Section interpreter.
           l ← interp_alloc n;
           _ ← interp_modify_state (state_init_heap l n v);
           mret (LitV (LitLoc l))
-        else (error $ if decide (n = 0)
+        else (error $ if decide (n = 0%Z)
                       then "alloc: cannot allocate 0 elements"
                       else "alloc: negative number of elements (first argument) " + n)
       | _ => error $ "alloc: number of elements (first argument) " + nv
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index cb7c84810285a63b361ba9d7ef6d8639528a8cb1..dbb6d172d17d11caf611d19c9987fbe2cf359f52 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -135,12 +135,12 @@ Section tests.
   Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1)%Z with (n:Z) by lia.
+    by replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat n) by lia.
   Qed.
   Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
   Proof.
     iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
-    by replace (S n - 1)%Z with (n:Z) by lia.
+    by replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat n) by lia.
   Qed.
 
   (* Make sure [wp_bind] works even when it changes nothing. *)
@@ -353,7 +353,9 @@ Section mapsto_tests.
   Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
 
   Lemma persistent_mapsto_load l (n : nat) :
-    {{{ l ↦ #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦□ #(n + 5) }}}.
+    {{{ l ↦ #n }}}
+      Store #l (! #l + #5) ;; ! #l
+    {{{ RET #(Z.of_nat n + 5); l ↦□ #(Z.of_nat n + 5) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ".
     wp_load. wp_store.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 9f2cc58424df35971260f7be5bb23812fa11cc9a..9765010e82998cc6897257e56c882f34456cd1e1 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -232,7 +232,7 @@ Section counter_proof.
       iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
       rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+      { iNext. iExists (S c). rewrite /LitNat Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. rewrite {3}/C; eauto 10.
     - wp_cmpxchg_fail; first (intros [=]; abstract lia).
       iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9d5336d56944da28a4d63c66ffd636ad3d6f0538..3b1c16fdd246a62c29a1e3ba6c7907c39f52e440 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -514,8 +514,8 @@ Proof.
 Qed.
 
 (* Check coercions *)
-Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
-Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
+Lemma test_iExist_coercion (P : Prop → PROP) : (∀ x, P x) -∗ ∃ x, P x.
+Proof. iIntros "HP". iExists false. iApply ("HP" $! false). Qed.
 
 Lemma test_iExist_tc `{Set_ A C} P : ⊢ ∃ x1 x2 : gset positive, P -∗ P.
 Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.