diff --git a/barrier/lifting.v b/barrier/lifting.v
index dd463d2d087d8d59a12b19a919d88b5822ceb10d..28a535e4dffa2ac2591a46f2e40f6b00b359e065 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -100,7 +100,7 @@ Lemma wp_le_true E n1 n2 Q :
   ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
-    last by intros; inv_step; eauto with lia.
+    last by intros; inv_step; eauto with omega.
   by rewrite -wp_value'.
 Qed.
 
@@ -109,7 +109,7 @@ Lemma wp_le_false E n1 n2 Q :
   ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
-    last by intros; inv_step; eauto with lia.
+    last by intros; inv_step; eauto with omega.
   by rewrite -wp_value'.
 Qed.
 
@@ -155,7 +155,7 @@ Lemma wp_le E n1 n2 P Q :
 Proof.
   intros; destruct (decide (n1 ≤ n2)).
   * rewrite -wp_le_true; auto.
-  * rewrite -wp_le_false; auto with lia.
+  * rewrite -wp_le_false; auto with omega.
 Qed.
 
 End lifting.
diff --git a/barrier/tests.v b/barrier/tests.v
index 4f0107b6d36a74f261c26a576140f2e1d88212c3..667e4f538703a23a2da4cf13373c5dcf83b262d6 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -90,7 +90,7 @@ Module LiftingTests.
     * rewrite -wp_case_inr //.
       rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
-      by replace n1 with (pred n2) by lia.
+      by replace n1 with (pred n2) by omega.
   Qed.
 
   Lemma Pred_spec n E Q :
@@ -101,10 +101,10 @@ Module LiftingTests.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.
-      by replace n with 0 by lia.
+      by replace n with 0 by omega.
     - rewrite -wp_case_inr //.
       rewrite -!later_intro -FindPred_spec.
-      auto using and_intro, const_intro with lia.
+      auto using and_intro, const_intro with omega.
   Qed.
 
   Goal ∀ E,
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 85c0fd52a54257bc9ffbad52eb355ea039478895..d5867ab6d90799e057fcc031ce9dc682005944e1 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -2,6 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose tactics that are used throughout
 the development. *)
+Require Import Omega.
 Require Export Psatz.
 Require Export prelude.base.
 
@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *)
 Hint Extern 998 (_ = _) => f_equal : f_equal.
 Hint Extern 999 => congruence : congruence.
 Hint Extern 1000 => lia : lia.
+Hint Extern 1000 => omega : omega.
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
 is rather efficient when having big hint databases, or expensive [Hint Extern]