diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 0474eb3a8b2d9fdb32cb6695c2190976b04b3c0e..0b473a7925775b4b536967dedbb2d3fe349609b8 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -93,7 +93,7 @@ Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
 Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
 Proof using Fcontr.
   intros; induction i as [|i IH]; simpl; [done|].
-  by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
+  by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last lia.
 Qed.
 Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
 Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 612620318bee52290b19cbe556676c69d31de315..1916b8f40d6c83ecb507c9d9fdbaf1f39c49796e 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -74,7 +74,7 @@ Section gmultiset.
     rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
     split. done. rewrite !gmultiset_op_union=> x.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
-    omega.
+    lia.
   Qed.
 End gmultiset.
 
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 1f20a1592f599f5d30382ef5e631c2761bb64e8c..c620e931f083f01dfd3dac9e28d803e2dc6dd121 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -68,11 +68,11 @@ Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
 Next Obligation.
   intros ? n c; rewrite /compl /list_compl.
   destruct (c 0) as [|x l] eqn:Hc0 at 1.
-  { by destruct (chain_cauchy c 0 n); auto with omega. }
-  rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
+  { by destruct (chain_cauchy c 0 n); auto with lia. }
+  rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last lia.
   apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
   destruct (decide (i < length (c n))); last first.
-  { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
+  { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with lia. }
   rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
   destruct (lookup_lt_is_Some_2 (c n) i) as [? Hcn]; first done.
   by rewrite Hcn.
@@ -310,7 +310,7 @@ Section properties.
   Lemma list_lookup_singletonM_ne i j x :
     i ≠ j →
     ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
-  Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
+  Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
   Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
   Proof.
     rewrite list_lookup_validN. split.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 6801268688cf11d35e1896a2ca5fde9644c806b1..32479f7998febcf33d80e75286fbf4b0e8cb1a35 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -179,7 +179,7 @@ Proof.
   move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
   destruct z as [z|]; last done. exfalso.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
-  eapply cmra_validN_le. eapply Hy. omega.
+  eapply cmra_validN_le. eapply Hy. lia.
 Qed.
 
 (** * Natural numbers  *)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 4eb180241f5c6d753fc8cd706782d10af3b14888..e68cec85d735f12b325f6cc3e92d65da47e8ef24 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -178,7 +178,7 @@ Section ofe.
   Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
   Proof.
     transitivity (c n); first by apply conv_compl. symmetry.
-    apply chain_cauchy. omega.
+    apply chain_cauchy. lia.
   Qed.
 
   Lemma discrete_iff n (x : A) `{!Discrete x} y : x ≡ y ↔ x ≡{n}≡ y.
@@ -292,9 +292,9 @@ Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
   intros A ? f ? n.
-  induction n as [|n IH]=> -[|i] //= ?; try omega.
+  induction n as [|n IH]=> -[|i] //= ?; try lia.
   - apply (contractive_0 f).
-  - apply (contractive_S f), IH; auto with omega.
+  - apply (contractive_S f), IH; auto with lia.
 Qed.
 
 Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
@@ -341,7 +341,7 @@ Section fixpoint.
     intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x).
     assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n).
     { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
-        eauto using contractive_0, contractive_S with omega. }
+        eauto using contractive_0, contractive_S with lia. }
     set (fp2 := compl {| chain_cauchy := Hcauch |}).
     assert (f fp2 ≡ fp2).
     { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
@@ -856,7 +856,7 @@ Section discrete_ofe.
     { compl c := c 0 }.
   Next Obligation.
     intros n c. rewrite /compl /=;
-    symmetry; apply (chain_cauchy c 0 n). omega.
+    symmetry; apply (chain_cauchy c 0 n). lia.
   Qed.
 End discrete_ofe.
 
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index b8981923b92d031b014c9d67e929315960edfdf4..4ebe5cccc7ae03383bc76cf0c0be2760fb0165c9 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -90,7 +90,7 @@ Proof.
     * rewrite comm -assoc. done.
     * rewrite comm -assoc. done.
     * exists y'. split=>//. by exists x'.
- - intros; assert (n' < a). omega.
+ - intros; assert (n' < a). lia.
     move: laterN_small. uPred.unseal.
     naive_solver.
 Qed.
@@ -178,22 +178,22 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
       case (decide (k' < n)).
       ** move: laterN_small; uPred.unseal; naive_solver.
       ** intros. exfalso. eapply HnnP; eauto.
-         assert (n ≤ k'). omega.
+         assert (n ≤ k'). lia.
          intros n'' x'' ???.
          specialize (HPF n'' x''). exfalso.
          eapply laterN_big; last (unseal; eauto).
-         eauto. omega.
+         eauto. lia.
     * inversion Hle; simpl; subst.
       ** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
          case (decide (k' < n)).
          *** move: laterN_small; uPred.unseal; naive_solver.
-         *** intros. exfalso. assert (n ≤ k'). omega.
-             assert (n = S k ∨ n < S k) as [->|] by omega.
+         *** intros. exfalso. assert (n ≤ k'). lia.
+             assert (n = S k ∨ n < S k) as [->|] by lia.
              **** eapply laterN_big; eauto; unseal.
                   eapply HnnP; eauto. move: HPF; by unseal.
              **** move:nnupd_k_elim. unseal. intros Hnnupdk.
                   eapply laterN_big; eauto. unseal.
-                  eapply (Hnnupdk n k); first omega; eauto.
+                  eapply (Hnnupdk n k); first lia; eauto.
                   exists x, x'. split_and!; eauto. eapply uPred_mono; eauto.
       ** intros HP. eapply IHk; auto.
          move:HP. unseal. intros (?&?); naive_solver.
@@ -265,7 +265,7 @@ Proof.
     exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
     * rewrite comm. done.
     * rewrite comm. done.
-  - intros; assert (n' < a). omega.
+  - intros; assert (n' < a). lia.
     move: laterN_small. uPred.unseal.
     naive_solver.
 Qed.
@@ -286,7 +286,7 @@ Proof using Type*.
   red; rewrite //= => n' x' ???.
   case (decide (n' = k)); intros.
   - subst. exfalso. eapply Hfal. rewrite (comm op); eauto.
-  - assert (n' < k). omega.
+  - assert (n' < k). lia.
     move: laterN_small. uPred.unseal. naive_solver.
 Qed.
 End classical.
@@ -306,7 +306,7 @@ Proof.
   split. unseal. intros n' ?? Hupd.
   case (decide (n' < n)).
   - intros. move: laterN_small. unseal. naive_solver.
-  - intros. assert (n ≤ n'). omega.
+  - intros. assert (n ≤ n'). lia.
     exfalso. specialize (Hupd n' ε).
     eapply Hdne. intros Hfal.
     eapply laterN_big; eauto.
@@ -326,14 +326,14 @@ Proof.
     specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
     intros Hf3. eapply Hf3; eauto.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
-    assert (n' < S k ∨ n' = S k) as [|] by omega.
+    assert (n' < S k ∨ n' = S k) as [|] by lia.
     * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall.
       eapply Hsmall; eauto.
     * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
   - intros k P x Hx. rewrite ?Nat_iter_S_r.
-    replace (S (S n) + k) with (S n + (S k)) by omega.
-    replace (S n + k) with (n + (S k)) by omega.
-    intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
+    replace (S (S n) + k) with (S n + (S k)) by lia.
+    replace (S n + k) with (n + (S k)) by lia.
+    intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by lia. eauto.
     rewrite ?Nat_iter_S_r. eauto.
 Qed.
 
@@ -356,7 +356,7 @@ Proof.
   destruct n.
   - rewrite //=; unseal; auto.
   - intros ??? Hfal.
-    eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by omega); eauto.
+    eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by lia); eauto.
     unseal. intros (x'&?&Hphi). simpl in *.
     eapply Hfal. auto.
 Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 5f1f20de0d7b30ad11936b54529fcf378206e6aa..6f04ccb5499337ada42a3eedcda6efbf1ac84db2 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -5,7 +5,7 @@ From Coq.Init Require Import Nat.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
-Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 10 (_ ≤ _) => lia.
 
 (** The basic definition of the uPred type, its metric and functor laws.
     You probably do not want to import this file. Instead, import
@@ -466,7 +466,7 @@ Qed.
 
 Lemma later_contractive : Contractive (@uPred_later M).
 Proof.
-  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try lia.
   apply HPQ; eauto using cmra_validN_S.
 Qed.
 
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 7e1a0c8704a2a10f632de4cf7ecd5dd085ddd49c..788eb85800e92526c9ea674b08cfee97001306fc 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -130,7 +130,7 @@ Section contrib_spec.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
+      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
       wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_if. by iApply "HΦ".
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 4b97fed7f36551fabe0007c2da5c1469a6713554..27fe865a6e30374af760222c7ab3dd7948079d4f 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -58,7 +58,7 @@ Proof.
   (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
   is very slow here *)
   do 18 (f_contractive || f_equiv). apply IH; first lia.
-  intros v. eapply dist_le; eauto with omega.
+  intros v. eapply dist_le; eauto with lia.
 Qed.
 Global Instance wp_proper s E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).