diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 5f74f033294982cb7e143c11cc7f7487e078ef16..c1a914da86c7c63c9b3c4fe0b9f0af9d575937cc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -104,17 +104,17 @@ Section tests.
     iIntros (Hn) "HΦ".
     iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
     wp_rec. wp_pures. case_bool_decide; wp_if.
-    - iApply ("IH" with "[%] [%] HΦ"); omega.
-    - by assert (n1' = n2 - 1) as -> by omega.
+    - iApply ("IH" with "[%] [%] HΦ"); lia.
+    - by assert (n1' = n2 - 1) as -> by lia.
   Qed.
 
   Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
   Proof.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide.
-    - wp_apply FindPred_spec; first omega. wp_pures.
-      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
-    - wp_apply FindPred_spec; eauto with omega.
+    - wp_apply FindPred_spec; first lia. wp_pures.
+      by replace (n - 1) with (- (-n + 2 - 1)) by lia.
+    - wp_apply FindPred_spec; eauto with lia.
   Qed.
 
   Lemma Pred_user E :
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 1822dfc3b0d03c522dfc98ac206712ac76a1dbd1..8539b5d44b81c6c73d4477c6b19891aa848b00d4 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -232,7 +232,7 @@ Section counter_proof.
       wp_cmpxchg_suc. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. rewrite {3}/C; eauto 10.
-    - wp_cmpxchg_fail; first (intros [=]; abstract omega).
+    - wp_cmpxchg_fail; first (intros [=]; abstract lia).
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
@@ -248,6 +248,6 @@ Section counter_proof.
     { iApply own_op. by iFrame. }
     rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
     iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    rewrite /C; eauto 10 with omega.
+    rewrite /C; eauto 10 with lia.
   Qed.
 End counter_proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index a68c061d10fb5cc4ccf3bcc7a9d0e8bb9b789e8d..6db8fd04f281394de05a14bf5e321d5ab35ac49c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -422,7 +422,7 @@ Lemma test_iInduction_wf (x : nat) P Q :
 Proof.
   iIntros "#HP HQ".
   iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
-  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first omega.
+  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
 Qed.
 
 Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y :
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index d7f1865a9444f75a39dfd962b5bc6f0a89f8a6c3..e2406fac957f2ddf9a55e30525cf2ab92f748bf3 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -48,7 +48,7 @@ Proof.
     wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
     wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
-    { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
+    { by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by lia. }
     iExists ll, lr, vl, vr. by iFrame.
 Qed.
 
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index a0637add5c6fc416c0b13100174e50e3852c6f7f..52e256df15fe2c168e632db254c1f05aecb17aac 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -46,7 +46,7 @@ Proof.
     iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
     rewrite !app_length /= !app_length.
     replace (length t1' + S (length t2' + length efs))
-      with (length efs + (length t1' + S (length t2'))) by omega. iFrame.
+      with (length efs + (length t1' + S (length t2'))) by lia. iFrame.
 Qed.
 
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :