replacing omega with lia in some file

1 files changed, 7 insertions, 6 deletions

diff --git a/common/Values.v b/common/Values.v
index 1d272932..c48dca25 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -20,6 +20,7 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
+Require Import Lia.
 
 Definition block : Type := positive.
 Definition eq_block := peq.
@@ -1535,14 +1536,14 @@ Proof.
     replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
     replace (Int.ltu n Int.iwordsize) with true.
     f_equal; apply Int.shrx_shr_2; assumption.
-    symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
+    symmetry; apply zlt_true. change (Int.unsigned n < 32); lia.
     symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
     assert (Int.unsigned n <> 0).
     { red; intros; elim H.
       rewrite <- (Int.repr_unsigned n), H0. auto. }
     rewrite Int.unsigned_repr.
-    change (Int.unsigned Int.iwordsize) with 32; omega.
-    assert (32 < Int.max_unsigned) by reflexivity. omega.
+    change (Int.unsigned Int.iwordsize) with 32; lia.
+    assert (32 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem or_rolm:
@@ -1848,12 +1849,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
   replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
   replace (Int.ltu n Int64.iwordsize') with true.
   f_equal; apply Int64.shrx'_shr_2; assumption.
-  symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
+  symmetry; apply zlt_true. change (Int.unsigned n < 64); lia.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
   rewrite Int.unsigned_repr.
-  change (Int.unsigned Int64.iwordsize') with 64; omega.
-  assert (64 < Int.max_unsigned) by reflexivity. omega.
+  change (Int.unsigned Int64.iwordsize') with 64; lia.
+  assert (64 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem negate_cmp_bool: