diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 8fe24c17104007aec8a1ba00de76d3cdc30fa1ca..2d8d2b3ddeec4d951d104b2b1ba158349ff230a2 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -148,7 +148,8 @@ Section seqZ.
   Proof.
     intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
     f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
-    apply list_fmap_ext; naive_solver auto with lia.
+    apply list_fmap_ext; [|done]; intros j; simpl.
+    rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
   Qed.
 
   Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i].
@@ -162,7 +163,7 @@ Section seqZ.
   Proof.
     rewrite elem_of_list_lookup.
     setoid_rewrite lookup_seqZ. split; [naive_solver lia|].
-    exists (Z.to_nat (k - m)). lia.
+    exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia.
   Qed.
 
   Lemma Forall_seqZ (P : Z → Prop) m n :