Fix compilation with Coq 8.10 (which has a weaker `lia`).

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 :