diff --git a/CHANGELOG.md b/CHANGELOG.md
index ce595d577fa1ba894d48f6d51fb21c1399159f95..ebe3c7c355e84296b21d279e735f78b39b5f358f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ API-breaking change is listed.
   + Add lemmas for `∈` and `∉` specific for multisets, since the set lemmas no
     longer work for multisets.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
+- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
 
 ## std++ 1.5.0
 
diff --git a/theories/hashset.v b/theories/hashset.v
index b6d8564229720bedd7f58a9b8ead956a07b1e1d4..72d865301af8f094832ef5b41a817c57dd3aff95 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -126,7 +126,7 @@ Definition remove_dups_fast (l : list A) : list A :=
   | [] => []
   | [x] => [x]
   | _ =>
-     let n : Z := length l in
+     let n : Z := Z.of_nat (length l) in
      elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
        hashset (λ x, hash x `mod` (2 * n))%Z)
   end.
@@ -134,7 +134,7 @@ Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
 Proof.
   destruct l as [|x1 [|x2 l]]; try reflexivity.
   unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
-  generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
+  generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f.
   rewrite elem_of_elements; split.
   - revert x. induction l as [|y l IH]; intros x; simpl.
     { by rewrite elem_of_empty. }
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 1bb5a81625c3f0c29748a41af9b9b4165701f3f0..43e5d06cbde6bacb514f1117bb5a5a87beb4a06a 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -7,7 +7,7 @@ From stdpp Require Import options.
 (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
 over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
 Definition seqZ (m len: Z) : list Z :=
-  (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
+  (λ i: nat, Z.add (Z.of_nat i) m) <$> (seq 0 (Z.to_nat len)).
 Global Arguments seqZ : simpl never.
 
 Definition sum_list_with {A} (f : A → nat) : list A → nat :=
@@ -107,7 +107,7 @@ Section seqZ.
       f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia.
     - by rewrite !seqZ_nil by lia.
   Qed.
-  Lemma lookup_seqZ_lt m n i : i < n → seqZ m n !! i = Some (m + i).
+  Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i).
   Proof.
     revert m i. induction n as [|n ? IH|] using (Z_succ_pred_induction 0);
       intros m i Hi; [lia| |lia].
@@ -115,9 +115,9 @@ Section seqZ.
     - f_equal; lia.
     - rewrite Z.pred_succ, IH by lia. f_equal; lia.
   Qed.
-  Lemma lookup_total_seqZ_lt m n i : i < n → seqZ m n !!! i = m + i.
+  Lemma lookup_total_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !!! i = m + Z.of_nat i.
   Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_lt. Qed.
-  Lemma lookup_seqZ_ge m n i : n ≤ i → seqZ m n !! i = None.
+  Lemma lookup_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !! i = None.
   Proof.
     revert m i.
     induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia.
@@ -126,11 +126,11 @@ Section seqZ.
       destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia.
     - by rewrite seqZ_nil by lia.
   Qed.
-  Lemma lookup_total_seqZ_ge m n i : n ≤ i → seqZ m n !!! i = inhabitant.
+  Lemma lookup_total_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !!! i = inhabitant.
   Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_ge. Qed.
-  Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + i ∧ i < n.
+  Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + Z.of_nat i ∧ Z.of_nat i < n.
   Proof.
-    destruct (Z_le_gt_dec n i).
+    destruct (Z_le_gt_dec n (Z.of_nat i)).
     - rewrite lookup_seqZ_ge by lia. naive_solver lia.
     - rewrite lookup_seqZ_lt by lia. naive_solver lia.
   Qed.
@@ -148,7 +148,7 @@ Section seqZ.
     rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
   Qed.
 
-  Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
+  Lemma seqZ_S m i : seqZ m (Z.of_nat (S i)) = seqZ m (Z.of_nat i) ++ [m + Z.of_nat i].
   Proof.
     unfold seqZ. rewrite !Nat2Z.id, seq_S, fmap_app.
     simpl. by rewrite Z.add_comm.
diff --git a/theories/numbers.v b/theories/numbers.v
index 670095229dc379a1bcdfe3da61c3d99f6c2b38b4..bce80ceb10a9d27fde9eba02dcce9f5f5c746a80 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -7,7 +7,6 @@ From stdpp Require Export base decidable option.
 From stdpp Require Import options.
 Local Open Scope nat_scope.
 
-Coercion Z.of_nat : nat >-> Z.
 Global Instance comparison_eq_dec : EqDecision comparison.
 Proof. solve_decision. Defined.
 
@@ -425,7 +424,7 @@ Global Hint Extern 1000 => lia : zpos.
 
 Lemma Z_to_nat_nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
 Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
-Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
+Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
 Proof.
   induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
   by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
@@ -443,18 +442,18 @@ Qed.
 Lemma Z2Nat_divide n m :
   0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
 Proof. intros. by rewrite <-Nat2Z_divide, !Z2Nat.id by done. Qed.
-Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = x `div` y.
+Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y).
 Proof.
   destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.div_unique with (x `mod` y)%nat.
+  apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat.
   { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
     apply Nat.mod_bound_pos; lia. }
   by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
 Qed.
-Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = x `mod` y.
+Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
 Proof.
   destruct (decide (y = 0%nat)); [by subst; destruct x |].
-  apply Z.mod_unique with (x `div` y)%nat.
+  apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat.
   { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
     apply Nat.mod_bound_pos; lia. }
   by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
@@ -463,7 +462,7 @@ Lemma Z2Nat_inj_div x y :
   0 ≤ x → 0 ≤ y →
   Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
 Proof.
-  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
+  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
   pose proof (Z.div_pos x y).
   apply (inj Z.of_nat). by rewrite Nat2Z_inj_div, !Z2Nat.id by lia.
 Qed.
@@ -471,7 +470,7 @@ Lemma Z2Nat_inj_mod x y :
   0 ≤ x → 0 ≤ y →
   Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
 Proof.
-  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
+  intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
   pose proof (Z_mod_pos x y).
   apply (inj Z.of_nat). by rewrite Nat2Z_inj_mod, !Z2Nat.id by lia.
 Qed.
@@ -1243,13 +1242,13 @@ lists, since the index [i] of [rotate n l] corresponds to the index
 [rotate_nat_add n i (length i)] of the original list. The definition
 uses [Z] for consistency with [rotate_nat_sub]. **)
 Definition rotate_nat_add (base offset len : nat) : nat :=
-  Z.to_nat ((base + offset) `mod` len)%Z.
+  Z.to_nat ((Z.of_nat base + Z.of_nat offset) `mod` Z.of_nat len)%Z.
 (** [rotate_nat_sub base offset len] is the inverse of [rotate_nat_add
 base offset len]. The definition needs to use modulo on [Z] instead of
 on nat since otherwise we need the sidecondition [base < len] on
 [rotate_nat_sub_add]. **)
 Definition rotate_nat_sub (base offset len : nat) : nat :=
-  Z.to_nat ((len + offset - base) `mod` len)%Z.
+  Z.to_nat ((Z.of_nat len + Z.of_nat offset - Z.of_nat base) `mod` Z.of_nat len)%Z.
 
 Lemma rotate_nat_add_add_mod base offset len:
   rotate_nat_add base offset len =
@@ -1299,7 +1298,7 @@ Lemma rotate_nat_sub_lt base offset len :
   0 < len → rotate_nat_sub base offset len < len.
 Proof.
   unfold rotate_nat_sub. intros ?.
-  pose proof (Z_mod_lt (len + offset - base) len).
+  pose proof (Z_mod_lt (Z.of_nat len + Z.of_nat offset - Z.of_nat base) (Z.of_nat len)).
   apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia.
 Qed.
 
@@ -1309,7 +1308,8 @@ Lemma rotate_nat_add_sub base len offset:
 Proof.
   intros ?. unfold rotate_nat_add, rotate_nat_sub.
   rewrite Z2Nat.id by (apply Z_mod_pos; lia). rewrite Zplus_mod_idemp_r.
-  replace (base + (len + offset - base))%Z with (len + offset)%Z by lia.
+  replace (Z.of_nat base + (Z.of_nat len + Z.of_nat offset - Z.of_nat base))%Z
+    with (Z.of_nat len + Z.of_nat offset)%Z by lia.
   rewrite (Zmod_in_range 1) by lia.
   rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
 Qed.
@@ -1320,9 +1320,11 @@ Lemma rotate_nat_sub_add base len offset:
 Proof.
   intros ?. unfold rotate_nat_add, rotate_nat_sub.
   rewrite Z2Nat.id by (apply Z_mod_pos; lia).
-  assert (∀ n, (len + n - base) = ((len - base) + n))%Z as -> by naive_solver lia.
+  assert (∀ n, (Z.of_nat len + n - Z.of_nat base) = ((Z.of_nat len - Z.of_nat base) + n))%Z
+    as -> by naive_solver lia.
   rewrite Zplus_mod_idemp_r.
-  replace (len - base + (base + offset))%Z with (len + offset)%Z by lia.
+  replace (Z.of_nat len - Z.of_nat base + (Z.of_nat base + Z.of_nat offset))%Z with
+    (Z.of_nat len + Z.of_nat offset)%Z by lia.
   rewrite (Zmod_in_range 1) by lia.
   rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
 Qed.