1 files changed, 3 insertions, 2 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 0f895040..5a7cfc12 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
+Require Import Lia.
 
 (** The abstract domains for value analysis *)
 
@@ -2822,8 +2823,8 @@ Proof.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
-    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
-    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
   }
   intros until y.
   intros HX HY.