Remove some stuff that's in the stdlib.

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).
 

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..|].

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. }

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. *)

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.