diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 73dd1d80ce8a44b6368e0a44f6edca837816c037..47f69d9baf88521f35c7e79b20beba7bdcfa3604 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -168,11 +168,8 @@ Qed.
 (** The stepping relation *)
 (* Be careful to make sure that poison is always stuck when used for anything
    except for reading from or writing to memory! *)
-Definition Z_of_bool (b : bool) : Z :=
-  if b then 1 else 0.
-
 Definition lit_of_bool (b : bool) : base_lit :=
-  LitInt $ Z_of_bool b.
+  LitInt $ Z.b2z b.
 
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index c0a81a94c82affa1422865c37f80660bf7d9054a..2a3dd10867a1fa4e3df0a68b0115aeab7e1d5722 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -78,7 +78,7 @@ Section join.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
     iApply (type_new_subtype (Π[uninit R_A.(ty_size); uninit R_B.(ty_size)]));
       (* FIXME: solve_typing should handle this without any aid. *)
-      rewrite ?Z_nat_add; [solve_typing..|].
+      rewrite ?Nat2Z.inj_add; [solve_typing..|].
     iIntros (r); simpl_subst.
     iApply (type_memcpy R_A); [solve_typing..|].
     iApply (type_memcpy R_B); [solve_typing..|].
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 9bf62cddfc1d934dca9eda0b70496385d19211ec..29ac59019e843d94168767e479c5f1f020fa6214 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -29,7 +29,7 @@ Section mutex.
        ty_own tid vl :=
          match vl return _ with
          | #(LitInt z) :: vl' =>
-           ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
+           ⌜∃ b, z = Z.b2z b⌝ ∗ ty.(ty_own) tid vl'
          | _ => False end;
        ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
            &at{κ, mutexN} (lock_proto l (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid)))
@@ -46,10 +46,10 @@ Section mutex.
     iDestruct "H" as "[>EQ Hown]". iDestruct "EQ" as %[b ->].
     (* We need to turn the ohne borrow into two, so we close it -- and then
        we open one of them again. *)
-    iMod ("Hclose" $! ((∃ b, l ↦ #(Z_of_bool b)) ∗ ((l +ₗ 1) ↦∗: ty_own ty tid))%I
+    iMod ("Hclose" $! ((∃ b, l ↦ #(Z.b2z b)) ∗ ((l +ₗ 1) ↦∗: ty_own ty tid))%I
           with "[] [Hl H↦ Hown]") as "[Hbor Htok]".
     { clear. iNext. iIntros "[Hl Hown] !>". iNext. iDestruct "Hl" as (b) "Hl".
-      iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z_of_bool b) :: vl).
+      iDestruct "Hown" as (vl) "[H↦ Hown]". iExists (#(Z.b2z b) :: vl).
       rewrite heap_mapsto_vec_cons. iFrame. iPureIntro. eauto. }
     { iNext. iSplitL "Hl"; first by eauto.
       iExists vl. iFrame. }
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 701bfc65b119e9e488f9f3074d7a34650763a495..55dd12a83468aeb21c7aadfa7bcbe27cc0591ab4 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -7,10 +7,6 @@ From iris.prelude Require Import options.
 Section product.
   Context `{!typeGS Σ}.
 
-  (* TODO: Find a better spot for this. *)
-  Lemma Z_nat_add (n1 n2 : nat) : Z.to_nat (n1 + n2) = (n1 + n2)%nat.
-  Proof. rewrite Z2Nat.inj_add; [|lia..]. rewrite !Nat2Z.id //. Qed.
-
   (* "Pre"-unit.  We later define the full unit as the empty product.  That's
      convertible, but products are opaque in some hint DBs, so this does make a
      difference. *)
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index a83b066e958ea17cb75dd8530679bf307d9e97cb..9038bc5c711503c9d5c14bf363d426ab51e87c5e 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -210,7 +210,7 @@ Section sum.
         iDestruct ("Htlclose" with "Htl") as "Htl".
         iDestruct (heap_mapsto_agree with "[Hown1 Hown2]") as "#Heq".
         { iDestruct "Hown1" as "[$ _]". iDestruct "Hown2" as "[$ _]". }
-        iDestruct "Heq" as %[= ->%Z_of_nat_inj].
+        iDestruct "Heq" as %[= ->%Nat2Z.inj].
         iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.