replacing omega with lia in some file

33 files changed, 296 insertions, 267 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 66aab49c..b975197a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -192,6 +192,8 @@ build_rv64:
   script:
     - ./config_rv64.sh
     - make -j "$NJOBS"
+    - export LD_LIBRARY_PATH=/usr/riscv64-linux-gnu/lib
+    - sudo ln -s /usr/riscv64-linux-gnu/lib/ld-linux-riscv64-lp64d.so.1 /lib
     - make -C test CCOMPOPTS=-static SIMU='qemu-riscv64' EXECUTE='qemu-riscv64' all test
     - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
   rules:
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index c606002a..073f1f4c 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -37,6 +37,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
 Require Import OptionMonad Asm.
+Require Import Lia.
 Require Export Asm.
 
 Local Open Scope option_monad_scope.
@@ -437,7 +438,7 @@ Qed.
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
   unfold size. destruct b as [hd bdy ex cor]. cbn.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega);
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia);
   unfold non_empty_bblockb in cor; simpl in cor.
   inversion cor.
 Qed.
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 6f7d39fa..11219928 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -19,6 +19,7 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock IterList.
 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
+Require Import Lia.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -71,7 +72,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
@@ -298,8 +299,8 @@ Proof.
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -389,7 +390,7 @@ Lemma mbsize_eqz:
 Proof.
   intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
   remember (length _) as a. remember (length_opt _) as b.
-  assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
+  assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
   inv H0. inv H1. destruct bdy; destruct ex; auto.
   all: try discriminate.
 Qed.
@@ -1452,11 +1453,11 @@ Proof.
       rewrite Pregmap.gso; auto. rewrite V; auto.
   } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
   exploit exec_straight_steps_2; eauto using functions_transl.
-  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
+  simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
   intros (ofs' & X & Y).
   left; exists (State rs3' m3'); split.
   eapply exec_straight_steps_1; eauto.
-  simpl fn_blocks. simpl fn_blocks in g. omega.
+  simpl fn_blocks. simpl fn_blocks in g. lia.
   constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -1495,7 +1496,7 @@ Local Transparent destroyed_at_function_entry.
 - (* return *) 
   inv MS.
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 03d863a3..004cfd5c 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -38,6 +38,7 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Asmblockprops.
+Require Import Lia.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. generalize (size_positive bi); intros; omega.
+  induction 1. lia. generalize (size_positive bi); intros; lia.
 Qed.
 
 Lemma find_bblock_tail:
@@ -405,10 +406,10 @@ Lemma find_bblock_tail:
 Proof.
   induction c1; simpl; intros.
   inversion H.  
-  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
-  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
   eauto.
 Qed.
 
@@ -422,13 +423,13 @@ Proof.
   induction 1; intros.
   - subst; eauto.
   - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
-    omega.
+    lia.
 Qed.
 
 Lemma size_blocks_pos c: 0 <= size_blocks c.
 Proof.
-  induction c as [| a l ]; simpl; try omega.
-  generalize (size_positive a); omega.
+  induction c as [| a l ]; simpl; try lia.
+  generalize (size_positive a); lia.
 Qed.
 
 Remark code_tail_positive:
@@ -436,15 +437,15 @@ Remark code_tail_positive:
   code_tail ofs fn c -> 0 <= ofs.
 Proof.
   induction 1; intros; simpl.
-  - omega.
-  - generalize (size_positive bi). omega.
+  - lia.
+  - generalize (size_positive bi). lia.
 Qed.
 
 Remark code_tail_size:
   forall fn ofs c,
   code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
 Proof.
-  induction 1; intros; simpl; try omega.
+  induction 1; intros; simpl; try lia.
 Qed.
 
 Remark code_tail_bounds fn ofs c:
@@ -453,7 +454,7 @@ Proof.
   intro H; 
   exploit code_tail_size; eauto.
   generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
-  omega.
+  lia.
 Qed.
 
 Local Hint Resolve code_tail_next: core.
@@ -470,8 +471,8 @@ Proof.
   intros.
   rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
   - rewrite Ptrofs.unsigned_repr; eauto.
-    omega.
-  - rewrite Ptrofs.unsigned_repr; omega.
+    lia.
+  - rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 (** The [find_label] function returns the code tail starting at the
@@ -505,12 +506,12 @@ Proof.
   simpl; intros until c'.
   case (is_label lbl a).
   - intros. inv H. exists pos. split; auto. split.
-    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
-    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+    replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
+    generalize (size_blocks_pos c). generalize (size_positive a). lia.
   - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
-  constructor. auto. generalize (size_positive a). omega.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
+  constructor. auto. generalize (size_positive a). lia.
 Qed.
 
 (** Predictor for return addresses in generated Asm code.
@@ -589,7 +590,7 @@ Proof.
     exists (Ptrofs.repr ofs). red; intros.
     rewrite Ptrofs.unsigned_repr. congruence.
     exploit code_tail_bounds; eauto.
-    intros; apply transf_function_len in TF. omega.
+    intros; apply transf_function_len in TF. lia.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -621,8 +622,8 @@ Remark code_tail_unique:
   code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
 Proof.
   induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
   f_equal. eauto.
 Qed.
 
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v
index 48840602..a5084b5f 100644
--- a/aarch64/PostpassSchedulingproof.v
+++ b/aarch64/PostpassSchedulingproof.v
@@ -21,6 +21,7 @@ Require Import Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -171,7 +172,7 @@ Proof.
   induction tc.
   - intros. simpl in H. discriminate.
   - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
-    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + inv H. assert (k = k') by lia. subst. reflexivity.
     + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
 Qed.
 
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 0716dad7..cf51f5a2 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -620,7 +620,7 @@ Proof.
   destruct a; simpl in H10; try discriminate; simpl; trivial.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite Z2Nat.id by omega.
+  rewrite H6. rewrite Z2Nat.id by lia.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 9e5ad6df..dd5e72f8 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -89,7 +89,7 @@ Qed.
 Obligation 2.
 Proof.
   simpl in BOUND.
-  omega.
+  lia.
 Qed.
 
 Program Definition bounded_nth_S_statement : Prop :=
@@ -104,14 +104,14 @@ Lemma bounded_nth_proof_irr :
          (BOUND1 BOUND2 : (k < List.length l)%nat),
     (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
 Proof.
-  induction k; destruct l; simpl; intros; trivial; omega.
+  induction k; destruct l; simpl; intros; trivial; lia.
 Qed.
 
 Lemma bounded_nth_S : bounded_nth_S_statement.
 Proof.
   unfold bounded_nth_S_statement.
   induction k; destruct l; simpl; intros; trivial.
-  1, 2: omega.
+  1, 2: lia.
   apply bounded_nth_proof_irr.
 Qed.
 
@@ -121,7 +121,7 @@ Lemma inject_list_injected:
     Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
 Proof.
   induction l; simpl; intros.
-  - omega.
+  - lia.
   - simpl.
     destruct k as [ | k]; simpl pos_add_nat.
     + simpl bounded_nth.
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.
diff --git a/common/Events.v b/common/Events.v
index 13741ebd..aff9e256 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -25,6 +25,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
+Require Import Lia.
 
 (** * Events and traces *)
 
@@ -1443,7 +1444,7 @@ Proof.
   econstructor; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - inv H; inv H0. exists Vundef, m1; constructor.
 (* determ *)
diff --git a/common/Memdata.v b/common/Memdata.v
index 1d651db2..6f04db36 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -23,6 +23,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
+Require Import Lia.
 
 (** * Properties of memory chunks *)
 
@@ -48,7 +49,7 @@ Definition largest_size_chunk := 8.
 
 Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
 Proof.
-  destruct chunk; simpl; omega.
+  destruct chunk; simpl; lia.
 Qed.
 
 Lemma size_chunk_pos:
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:
diff --git a/config_simple.sh b/config_simple.sh
index e2d3844c..a394e23f 100755
--- a/config_simple.sh
+++ b/config_simple.sh
@@ -5,7 +5,7 @@ branch=`git rev-parse --abbrev-ref HEAD`
 date=`date -I`
 
 if test "x$CCOMP_INSTALL_PREFIX" = "x" ;
-then CCOMP_INSTALL_PREFIX=/opt/CompCert ;
+then CCOMP_INSTALL_PREFIX=/home/yuki/Work/VERIMAG/CompCert ;
 fi
 
 ./configure --prefix ${CCOMP_INSTALL_PREFIX}/${branch}/${date}_${version}/$arch "$@" $arch
diff --git a/kvx/Asmblock.v b/kvx/Asmblock.v
index 64b2c535..17ebac32 100644
--- a/kvx/Asmblock.v
+++ b/kvx/Asmblock.v
@@ -29,6 +29,7 @@ Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
+Require Import Lia.
 
 (* Notations necessary to hook Asmvliw definitions *)
 Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs.
@@ -212,7 +213,7 @@ Qed.
 Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
 Proof.
   intros. destruct l; try (contradict H; auto; fail).
-  cbn. omega.
+  cbn. lia.
 Qed.
 
 Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
@@ -226,7 +227,7 @@ Qed.
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
   unfold size. destruct b as [hd bdy ex cor]. cbn.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega).
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia).
   inversion cor; contradict H; cbn; auto.
 Qed.
 
diff --git a/kvx/Asmblockgenproof.v b/kvx/Asmblockgenproof.v
index df1a070f..6e3029d8 100644
--- a/kvx/Asmblockgenproof.v
+++ b/kvx/Asmblockgenproof.v
@@ -21,6 +21,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.
 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 Require Import Axioms.
+Require Import Lia.
 
 Module MB := Machblock.
 Module AB := Asmvliw.
@@ -72,7 +73,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
@@ -247,8 +248,8 @@ Proof.
   split. unfold goto_label. unfold par_goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -1374,7 +1375,7 @@ Lemma mbsize_eqz:
 Proof.
   intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
   remember (length _) as a. remember (length_opt _) as b.
-  assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
+  assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
   inv H0. inv H1. destruct bdy; destruct ex; auto.
   all: try discriminate.
 Qed.
@@ -1706,11 +1707,11 @@ Proof.
       + contradiction.
   } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
   exploit exec_straight_steps_2; eauto using functions_transl.
-  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
+  simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
   intros (ofs' & X & Y).                    
   left; exists (State rs3' m3'); split.
   eapply exec_straight_steps_1; eauto.
-  simpl fn_blocks. simpl fn_blocks in g. omega.
+  simpl fn_blocks. simpl fn_blocks in g. lia.
   constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -1756,7 +1757,7 @@ Local Transparent destroyed_at_function_entry.
 - (* return *) 
   inv MS.
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.
diff --git a/kvx/Asmblockgenproof0.v b/kvx/Asmblockgenproof0.v
index 12bb863a..83b574e7 100644
--- a/kvx/Asmblockgenproof0.v
+++ b/kvx/Asmblockgenproof0.v
@@ -37,6 +37,7 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Asmblockprops.
+Require Import Lia.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -410,7 +411,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. generalize (size_positive bi); intros; omega.
+  induction 1. lia. generalize (size_positive bi); intros; lia.
 Qed.
 
 Lemma find_bblock_tail:
@@ -420,10 +421,10 @@ Lemma find_bblock_tail:
 Proof.
   induction c1; simpl; intros.
   inversion H.  
-  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
-  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
   eauto.
 Qed.
 
@@ -438,13 +439,13 @@ Proof.
   induction 1; intros.
   - subst; eauto.
   - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
-    omega.
+    lia.
 Qed.
 
 Lemma size_blocks_pos c: 0 <= size_blocks c.
 Proof.
-  induction c as [| a l ]; simpl; try omega.
-  generalize (size_positive a); omega.
+  induction c as [| a l ]; simpl; try lia.
+  generalize (size_positive a); lia.
 Qed.
 
 Remark code_tail_positive:
@@ -452,15 +453,15 @@ Remark code_tail_positive:
   code_tail ofs fn c -> 0 <= ofs.
 Proof.
   induction 1; intros; simpl.
-  - omega.
-  - generalize (size_positive bi). omega.
+  - lia.
+  - generalize (size_positive bi). lia.
 Qed.
 
 Remark code_tail_size:
   forall fn ofs c,
   code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
 Proof.
-  induction 1; intros; simpl; try omega.
+  induction 1; intros; simpl; try lia.
 Qed.
 
 Remark code_tail_bounds fn ofs c:
@@ -469,7 +470,7 @@ Proof.
   intro H; 
   exploit code_tail_size; eauto.
   generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
-  omega.
+  lia.
 Qed.
 
 Local Hint Resolve code_tail_next: core.
@@ -486,8 +487,8 @@ Proof.
   intros.
   rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
   - rewrite Ptrofs.unsigned_repr; eauto.
-    omega.
-  - rewrite Ptrofs.unsigned_repr; omega.
+    lia.
+  - rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 (** Predictor for return addresses in generated Asm code.
@@ -566,7 +567,7 @@ Proof.
     exists (Ptrofs.repr ofs). red; intros.
     rewrite Ptrofs.unsigned_repr. congruence.
     exploit code_tail_bounds; eauto.
-    intros; apply transf_function_len in TF. omega.
+    intros; apply transf_function_len in TF. lia.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -590,7 +591,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -598,8 +599,8 @@ Remark code_tail_unique:
   code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
 Proof.
   induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
   f_equal. eauto.
 Qed.
 
@@ -638,12 +639,12 @@ Proof.
   simpl; intros until c'.
   case (is_label lbl a).
   - intros. inv H. exists pos. split; auto. split.
-    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
-    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+    replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
+    generalize (size_blocks_pos c). generalize (size_positive a). lia.
   - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
-  constructor. auto. generalize (size_positive a). omega.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
+  constructor. auto. generalize (size_positive a). lia.
 Qed.
 
 (** Helper lemmas to reason about
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
index c6ad70ab..a65bd5bc 100644
--- a/kvx/Asmblockgenproof1.v
+++ b/kvx/Asmblockgenproof1.v
@@ -20,6 +20,7 @@ Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
 Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
 Require Import Chunks.
+Require Import Lia.
 
 Import PArithCoercions.
 
@@ -1466,7 +1467,7 @@ Proof.
   change (Int.unsigned Int.zero) with 0.
   pose proof (Int.unsigned_range x) as RANGE.
   unfold zlt, zeq.
-  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia.
 Qed.
 
 Lemma int64_ltu_to_neq:
@@ -1478,7 +1479,7 @@ Proof.
   change (Int64.unsigned Int64.zero) with 0.
   pose proof (Int64.unsigned_range x) as RANGE.
   unfold zlt, zeq.
-  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia.
 Qed.
 
 Ltac splitall := repeat match goal with |- _ /\ _ => split end.
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 8afe8d07..aa2e0885 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -32,6 +32,7 @@ Require Import Conventions.
 Require Import Errors.
 Require Import Sorting.Permutation.
 Require Import Chunks.
+Require Import Lia.
 
 (** * Abstract syntax *)
 
@@ -1709,7 +1710,7 @@ Ltac Det_WIO X :=
     split. auto. intros. destruct B; auto. subst. auto.
 - (* trace length *)
   red; intros. inv H; cbn.
-  omega.
+  lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 - (* initial states *)
diff --git a/kvx/ConstpropOpproof.v b/kvx/ConstpropOpproof.v
index ffd35bcc..f67b8a4e 100644
--- a/kvx/ConstpropOpproof.v
+++ b/kvx/ConstpropOpproof.v
@@ -19,6 +19,7 @@ Require Import Coqlib Compopts.
 Require Import Integers Floats Values Memory Globalenvs Events.
 Require Import Op Registers RTL ValueDomain.
 Require Import ConstpropOp.
+Require Import Lia.
 
 Section STRENGTH_REDUCTION.
 
@@ -336,7 +337,7 @@ Proof.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
   rewrite Int.bits_zero. cbn. rewrite andb_true_r. auto.
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
   econstructor; split; eauto. auto.
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index a0c10ddd..b4e14898 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -17,6 +17,7 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 Require Import Floats ExtFloats.
+Require Import Lia.
 
 Open Scope Z_scope.
 
@@ -31,9 +32,9 @@ Proof.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
-  - rewrite Z.abs_eq; omega.
-  - rewrite Z.abs_neq; omega.
-  - rewrite Z.abs_eq; omega.
+  - rewrite Z.abs_eq; lia.
+  - rewrite Z.abs_neq; lia.
+  - rewrite Z.abs_eq; lia.
 Qed.
 
 Inductive shift1_4 : Type :=
@@ -202,9 +203,9 @@ Proof.
   intros i H.
   destruct H as [Hlow Hhigh].
   apply Int64.unsigned_repr.
-  split. { omega. }
+  split. { lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
   
 Theorem divu_is_divlu: forall v1 v2 : val,
@@ -237,7 +238,7 @@ Proof.
   {subst i0_val.
    pose proof modulus_fits_64.
    rewrite Zdiv_1_r.
-   omega.
+   lia.
   }
   destruct (Z.eq_dec i_val 0).
   { subst i_val. compute.
@@ -245,11 +246,11 @@ Proof.
     intro ABSURD;
     discriminate ABSURD. }
   assert ((i_val / i0_val) < i_val).
-  { apply Z_div_lt; omega. }
+  { apply Z_div_lt; lia. }
   split.
-  { apply Z_div_pos; omega. }
+  { apply Z_div_pos; lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
   
 Theorem modu_is_modlu: forall v1 v2 : val,
@@ -280,12 +281,12 @@ Proof.
   reflexivity.
   assert((i_val mod i0_val) < i0_val).
   apply Z_mod_lt.
-  omega.
+  lia.
   split.
   { apply Z_mod_lt.
-    omega. }
+    lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
 
 Remark if_zlt_0_half_modulus :
@@ -332,7 +333,7 @@ Proof.
   set (y := Int64.unsigned (Int64.repr x)) in *.
   rewrite H64.
   clear H64.
-  omega.
+  lia.
 Qed.
 
 (*
@@ -375,15 +376,15 @@ Proof.
     destruct (zlt i0_val Int.half_modulus) as [Hlt_half | Hge_half].
     {
       replace Int.half_modulus with 2147483648 in * by reflexivity.
-      rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; omega).
-      destruct (zeq _ _) as [ | Hneq0]; try omega. clear Hneq0.
+      rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+      destruct (zeq _ _) as [ | Hneq0]; try lia. clear Hneq0.
       unfold Val.loword.
       f_equal.
       unfold Int64.divs, Int.divs, Int64.loword.
       unfold Int.signed, Int64.signed. cbn.      
       rewrite if_zlt_min_signed_half_modulus.
       change Int.half_modulus with 2147483648 in *.
-      destruct (zlt _ _) as [discard|]; try omega. clear discard.
+      destruct (zlt _ _) as [discard|]; try lia. clear discard.
       change (Int64.unsigned
                   (Int64.repr
                      (Int.unsigned (Int.repr Int.min_signed) - Int.modulus)))
@@ -391,8 +392,8 @@ Proof.
       change Int64.half_modulus with 9223372036854775808.
       change Int64.modulus with 18446744073709551616.
       cbn.
-      rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; omega).
-      destruct (zlt i0_val 9223372036854775808) as [discard |]; try omega.
+      rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; lia).
+      destruct (zlt i0_val 9223372036854775808) as [discard |]; try lia.
       clear discard.
       change (Int.unsigned (Int.repr Int.min_signed) - Int.modulus) with  (-2147483648).
       destruct (Z.eq_dec i0_val 1) as [H1 | Hnot1].
@@ -418,14 +419,14 @@ Proof.
       set (delta := (i0_val - Int.modulus)) in *.
       assert (delta = Int64.modulus*(delta/Int64.modulus)) as Hdelta.
       { apply Z_div_exact_full_2.
-        compute. omega.
+        compute. lia.
         assumption. }
       set (k := (delta / Int64.modulus)) in *.
       change Int64.modulus with 18446744073709551616 in *.
       change Int.modulus with 4294967296 in *.
       change Int.half_modulus with 2147483648 in *.
       change (Int.unsigned Int.mone) with 4294967295 in *.
-      omega.
+      lia.
     }
     unfold Int.divs, Int64.divs, Val.loword, Int64.loword.
     change (Int.unsigned (Int.repr Int.min_signed)) with 2147483648.
@@ -451,7 +452,7 @@ Proof.
   intro BIG.
   unfold Int.signed, Int.unsigned in *. cbn in *.
   destruct (zlt _ _).
-  omega.
+  lia.
   trivial.
 Qed.
 
@@ -476,11 +477,11 @@ Proof.
     subst.
     rewrite Z.quot_0_l.
     auto with zarith.
-    omega.
+    lia.
   }
   assert ((Z.quot a b) < a).
   {
-    apply Z.quot_lt; omega.
+    apply Z.quot_lt; lia.
   }
   auto with zarith.
 Qed.
@@ -516,9 +517,9 @@ Proof.
       change (Int.unsigned (Int.repr Int.min_signed)) with (2147483648) in *.
       rewrite big_unsigned_signed.
       change Int.modulus with 4294967296.
-      omega.
+      lia.
       change Int.half_modulus with 2147483648.
-      omega.
+      lia.
     }
     unfold Int.eq in EXCEPTION.
     destruct (zeq _ _) in EXCEPTION; try discriminate.
@@ -552,8 +553,8 @@ Lemma Z_quot_pos_pos_bound: forall a b m,
 Proof.
   intros.
   split.
-  { rewrite <- (Z.quot_0_l b) by omega.
-    apply Z_quot_monotone; omega.
+  { rewrite <- (Z.quot_0_l b) by lia.
+    apply Z_quot_monotone; lia.
   }
   apply Z.le_trans with (m := a).
   {
@@ -566,10 +567,10 @@ Lemma Z_quot_neg_pos_bound: forall a b m,
   intros.
   assert (0 <= - (a ÷ b) <= -m).
   {
-    rewrite <- Z.quot_opp_l by omega.
-    apply Z_quot_pos_pos_bound; omega.
+    rewrite <- Z.quot_opp_l by lia.
+    apply Z_quot_pos_pos_bound; lia.
   }
-  omega.
+  lia.
 Qed.
 
 Lemma Z_quot_signed_pos_bound: forall a b,
@@ -580,7 +581,7 @@ Proof.
   destruct (Z_lt_ge_dec a 0).
   {
     split.
-    { apply Z_quot_neg_pos_bound; omega. }
+    { apply Z_quot_neg_pos_bound; lia. }
     { eapply Z.le_trans with (m := 0).
       { apply Z_quot_neg_pos_bound with (m := Int.min_signed); trivial.
         split. tauto. auto with zarith.
@@ -592,9 +593,9 @@ Proof.
     { eapply Z.le_trans with (m := 0).
       discriminate.
       apply Z_quot_pos_pos_bound with (m := Int.max_signed); trivial.
-      split. omega. tauto.
+      split. lia. tauto.
     }
-    { apply Z_quot_pos_pos_bound; omega.
+    { apply Z_quot_pos_pos_bound; lia.
     }
   }
 Qed.
@@ -608,42 +609,42 @@ Proof.
   intros.
 
   replace b with (-(-b)) by auto with zarith.
-  rewrite Z.quot_opp_r by omega.
+  rewrite Z.quot_opp_r by lia.
   assert (-2147483647 <= (a ÷ - b) <= 2147483648).
-  2: omega.
+  2: lia.
   
   destruct (Z_lt_ge_dec a 0).
   {
     replace a with (-(-a)) by auto with zarith.
-    rewrite Z.quot_opp_l by omega.
+    rewrite Z.quot_opp_l by lia.
     assert (-2147483648 <= - a ÷ - b <= 2147483647).
-    2: omega.
+    2: lia.
     split.
     {
-      rewrite Z.quot_opp_l by omega.
+      rewrite Z.quot_opp_l by lia.
       assert (a ÷ - b <= 2147483648).
-      2: omega.
+      2: lia.
       {
         apply Z.le_trans with (m := 0).
-        rewrite <- (Z.quot_0_l (-b)) by omega.
-        apply Z_quot_monotone; omega.
+        rewrite <- (Z.quot_0_l (-b)) by lia.
+        apply Z_quot_monotone; lia.
         discriminate.
       }
     }
     assert (- a ÷ - b < -a ).
-    2: omega.
-    apply Z_quot_lt; omega.
+    2: lia.
+    apply Z_quot_lt; lia.
   }
   {
     split.
     { apply Z.le_trans with (m := 0).
       discriminate.
-      rewrite <- (Z.quot_0_l (-b)) by omega.
-      apply Z_quot_monotone; omega.
+      rewrite <- (Z.quot_0_l (-b)) by lia.
+      apply Z_quot_monotone; lia.
     }
     { apply Z.le_trans with (m := a).
       apply Z_quot_le.
-      all: omega.
+      all: lia.
     }
   }
 Qed.
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index f636336d..4578b4e8 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -18,6 +18,7 @@ Require Import AST Integers Floats.
 Require Import Values Memory Globalenvs.
 Require Import Op RTL.
 Require Import NeedDomain.
+Require Import Lia.
 
 (** Neededness analysis for RISC-V operators *)
 
@@ -405,8 +406,8 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply sign_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply sign_ext_redundant_sound; auto. lia.
 - apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v
index 1f1f238a..08e640c6 100644
--- a/kvx/PostpassScheduling.v
+++ b/kvx/PostpassScheduling.v
@@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
 Require Peephole.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -87,8 +88,8 @@ Lemma concat2_zlt_size:
 Proof.
   intros. monadInv H.
   split.
-  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
-  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
+  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. lia.
+  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. lia.
 Qed.
 
 Lemma concat2_noexit:
@@ -436,7 +437,7 @@ Lemma verified_schedule_size:
 Proof.
   intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
   all: try (apply verified_schedule_nob_size; auto; fail).
-  inv H. simpl. omega.
+  inv H. simpl. lia.
 Qed.
 
 Lemma verified_schedule_no_header_in_middle:
diff --git a/kvx/PostpassSchedulingproof.v b/kvx/PostpassSchedulingproof.v
index c290387b..937b3be6 100644
--- a/kvx/PostpassSchedulingproof.v
+++ b/kvx/PostpassSchedulingproof.v
@@ -20,6 +20,7 @@ Require Import Asmblockgenproof0 Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -93,12 +94,12 @@ Proof.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
-      repeat (rewrite Nat2Z.inj_add). omega. }
+      repeat (rewrite Nat2Z.inj_add). lia. }
     clear EXA H0 H1. rewrite H in EXEB.
     assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
     rewrite H0. rewrite <- pc_set_add; auto.
-    exploit size_positive. instantiate (1 := a). intro. omega.
-    exploit size_positive. instantiate (1 := b). intro. omega.
+    exploit size_positive. instantiate (1 := a). intro. lia.
+    exploit size_positive. instantiate (1 := b). intro. lia.
 Qed.
 
 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
@@ -140,7 +141,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma symbols_preserved:
@@ -224,7 +225,7 @@ Proof.
     + apply IHlbb in H. destruct H as (c & TAIL). exists c.
       enough (pos = pos - size a + size a) as ->.
       apply code_tail_S; auto.
-      omega.
+      lia.
 Qed.
 
 Lemma code_tail_head_app:
@@ -291,7 +292,7 @@ Lemma verified_schedule_not_empty:
   verified_schedule bb = OK lbb -> lbb <> nil.
 Proof.
   intros. apply verified_schedule_size in H.
-  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
+  pose (size_positive bb). assert (size_blocks lbb > 0) by lia. clear H g.
   destruct lbb; simpl in *; discriminate.
 Qed.
 
@@ -356,7 +357,7 @@ Proof.
   induction tc.
   - intros. simpl in H. discriminate.
   - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
-    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + inv H. assert (k = k') by lia. subst. reflexivity.
     + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
 Qed.
 
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index fb38bbce..c3abdbc7 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -23,6 +23,7 @@ Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 Require Import DecBoolOps.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -408,14 +409,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int64.zwordsize
-                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int64.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia.
         simpl.
         destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial.
         destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial.
@@ -460,14 +461,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int64.zwordsize
-                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int64.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia.
         simpl.
         destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial.
         destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial.
@@ -708,9 +709,9 @@ Proof.
                rewrite Int64.shl'_zero.
                reflexivity.
            *** simpl. unfold Int.max_unsigned. unfold Int.modulus.
-               simpl. omega.
+               simpl. lia.
         ** unfold Int.max_unsigned. unfold Int.modulus.
-               simpl. omega.
+               simpl. lia.
       * TrivialExists.
     + TrivialExists.
 - TrivialExists.
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 7a301929..a7169881 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -34,6 +34,7 @@ Require Import Events.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
 Require Import DecBoolOps.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -465,14 +466,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int.zwordsize
-                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by lia.
         rewrite Int.repr_unsigned.
         rewrite Int.repr_unsigned.
         simpl.
@@ -522,14 +523,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int.zwordsize
-                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by lia.
         rewrite Int.repr_unsigned.
         rewrite Int.repr_unsigned.
         simpl.
@@ -618,20 +619,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zbits.Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shr' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 - TrivialExists.
 Qed.
 
@@ -646,20 +647,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zbits.Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shru' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 - TrivialExists.
 Qed.
 
@@ -811,10 +812,10 @@ Proof.
         *** simpl.
             unfold Int.max_unsigned, Int.modulus.
             simpl.
-            omega.
+            lia.
         ** unfold Int.max_unsigned, Int.modulus.
            simpl.
-           omega.
+           lia.
       * apply DEFAULT.
     + apply DEFAULT.
   - apply DEFAULT.
diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v
index 81ffcebb..05cfa1d7 100644
--- a/kvx/Stacklayout.v
+++ b/kvx/Stacklayout.v
@@ -18,6 +18,7 @@
 Require Import Coqlib.
 Require Import AST Memory Separation.
 Require Import Bounds.
+Require Import Lia.
 
 Local Open Scope sep_scope.
 
@@ -71,15 +72,15 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -92,11 +93,11 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split_2. fold olink; omega. omega.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_split_2. fold olink; lia. lia.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -112,16 +113,16 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le. omega. 
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le. lia. 
 Qed.
 
 Lemma frame_env_aligned:
@@ -140,11 +141,11 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. apply Z.divide_0_r.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl.
 Qed.
diff --git a/lib/Integers.v b/lib/Integers.v
index c48af2fc..6143ab55 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -18,6 +18,7 @@
 Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits Axioms.
 Require Archi.
+Require Import Lia.
 
 (** * Comparisons *)
 
@@ -1205,20 +1206,20 @@ Proof.
   simpl.
   pose proof half_modulus_pos as HMOD.
   destruct (zlt 0 half_modulus) as [HMOD' | HMOD'].
-  2: omega.
+  2: lia.
   clear HMOD'.
   destruct (zlt (intval x) half_modulus) as [ LOW | HIGH].
   {
     destruct x as [ix RANGE].
     simpl in *.
-    destruct (zlt ix 0). omega.
+    destruct (zlt ix 0). lia.
     reflexivity.
   }
   destruct (zlt _ _) as [LOW' | HIGH']; trivial.
   destruct x as [ix RANGE].
   simpl in *.
   rewrite half_modulus_modulus in *.
-  omega.
+  lia.
 Qed.
 Local Opaque repr.
 
@@ -2482,20 +2483,20 @@ Proof.
       clear H.
       rewrite two_power_nat_two_p.
       split.
-      omega.
+      lia.
       set (w := (Z.of_nat wordsize)) in *.
       assert ((two_p 2) <= (two_p w)) as MONO.
       {
         apply two_p_monotone.
-        omega.
+        lia.
       }
       change (two_p 2) with 4 in MONO.
-      omega.
+      lia.
     }
     generalize wordsize_max_unsigned.
     fold zwordsize.
     generalize wordsize_pos.
-    omega.
+    lia.
   }
   rewrite unsigned_repr by assumption.
   simpl.
@@ -3677,27 +3678,27 @@ Lemma shr'63:
 Proof.
   intro.
   unfold shr', mone, zero.
-  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega).
+  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
   apply same_bits_eq.
   intros i BIT.
   rewrite testbit_repr by assumption.
-  rewrite Z.shiftr_spec by omega.
-  rewrite bits_signed by omega.
+  rewrite Z.shiftr_spec by lia.
+  rewrite bits_signed by lia.
   simpl.
   change zwordsize with 64 in *.
   destruct (zlt _ _) as [LT | GE].
   {
-    replace i with 0 in * by omega.
+    replace i with 0 in * by lia.
     change (0 + 63) with (zwordsize - 1).
     rewrite  sign_bit_of_signed.
     destruct (lt x _).
-    all: rewrite testbit_repr by (change zwordsize with 64 in *; omega).
+    all: rewrite testbit_repr by (change zwordsize with 64 in *; lia).
     all: simpl; reflexivity.
   }
   change (64 - 1) with (zwordsize - 1).
   rewrite  sign_bit_of_signed.
   destruct (lt x _).
-  all: rewrite testbit_repr by (change zwordsize with 64 in *; omega).
+  all: rewrite testbit_repr by (change zwordsize with 64 in *; lia).
   { symmetry.
     apply Ztestbit_m1.
     tauto.
@@ -3711,11 +3712,11 @@ Lemma shru'63:
 Proof.
   intro.
   unfold shru'.
-  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega).
+  rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia).
   apply same_bits_eq.
   intros i BIT.
   rewrite testbit_repr by assumption.
-  rewrite Z.shiftr_spec by omega.
+  rewrite Z.shiftr_spec by lia.
   unfold lt.
   rewrite signed_zero.
   unfold one, zero.
@@ -3728,15 +3729,15 @@ Proof.
       rewrite sign_bit_of_signed.
       unfold lt.
       rewrite signed_zero.
-      destruct (zlt _ _); try omega.
+      destruct (zlt _ _); try lia.
       reflexivity.
     }
     change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)).
-    rewrite bits_above by (change zwordsize with 64; omega).
+    rewrite bits_above by (change zwordsize with 64; lia).
     rewrite Ztestbit_1.
     destruct (zeq i 0); trivial.
     subst i.
-    omega.
+    lia.
   }
   destruct (zeq i 0) as [IZERO | INONZERO].
   { subst i.
@@ -3745,14 +3746,14 @@ Proof.
     unfold lt.
     rewrite signed_zero.
     rewrite bits_zero.
-    destruct (zlt _ _); try omega.
+    destruct (zlt _ _); try lia.
     reflexivity.
   }
   change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)).
   rewrite bits_zero.
   apply bits_above.
   change zwordsize with 64.
-  omega.
+  lia.
 Qed.
   
 Theorem shrx'1_shr':
diff --git a/lib/IterList.v b/lib/IterList.v
index bde47068..d28124c7 100644
--- a/lib/IterList.v
+++ b/lib/IterList.v
@@ -1,4 +1,5 @@
 Require Import Coqlib.
+Require Import Lia.
 
 (** TODO: are these def and lemma already defined in the standard library ?
 
@@ -55,17 +56,17 @@ Qed.
 Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
 Proof.
   unfold iter_tail; induction n; auto.
-  intros l; destruct l. { simpl; omega. }
+  intros l; destruct l. { simpl; lia. }
   intros; simpl. erewrite IHn; eauto.
-  simpl in *; omega.
+  simpl in *; lia.
 Qed.
 
 Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
 Proof.
   unfold iter_tail; induction n; simpl.
-  - intros l; destruct l; simpl; omega || eauto.
+  - intros l; destruct l; simpl; lia || eauto.
   - intros l H; destruct (IHn (tl l)) as (x & H1).
-    + destruct l; simpl in *; try omega.
+    + destruct l; simpl in *; try lia.
     + rewrite H1; eauto.
 Qed.
 
@@ -74,20 +75,20 @@ Proof.
   intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
   rewrite EQ.
   rewrite (length_iter_tail n2 l); eauto.
-  omega.
+  lia.
 Qed.
 
 Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
 Proof.
-  destruct (le_lt_dec n (List.length l)); try omega.
-  intros; exploit (iter_tail_inject1 n (length l) l); try omega.
+  destruct (le_lt_dec n (List.length l)); try lia.
+  intros; exploit (iter_tail_inject1 n (length l) l); try lia.
   rewrite iter_tail_reach_nil. auto.
 Qed.
 
 Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l).
 Proof.
   induction l; auto.
-  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega.
+  rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. lia.
 Qed.
 
 Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l).
@@ -99,13 +100,13 @@ Lemma is_tail_list_nth_z A (l1 l2: list A):
   is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
 Proof.
   induction 1; simpl.
-  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
+  - replace (list_length_z c - list_length_z c) with 0; lia || auto.
   - assert (X: list_length_z (i :: c2) > list_length_z c1).
     { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
       exploit is_tail_bound; simpl; eauto.
-      omega. }
-    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
+      lia. }
+    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try lia.
     replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
     rewrite list_length_z_cons.
-    omega.
+    lia.
 Qed.
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 6a0297e9..2669d4bc 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -524,7 +524,7 @@ Remark ltu_12_wordsize:
 Proof.
   unfold Int.iwordsize, Int.zwordsize. simpl.
   unfold Int.ltu. apply zlt_true.
-  rewrite !Int.unsigned_repr; try cbn; try omega.
+  rewrite !Int.unsigned_repr; try cbn; try lia.
 Qed.
 
 (* Signed longs *)
@@ -575,14 +575,14 @@ Proof.
   intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
   unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
   destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
   rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
   specialize (Int.eq_spec n (Int.repr Int.max_signed)).
   rewrite EQMAX; simpl; intros.
   assert (Int.signed n <> Int.max_signed).
   { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); omega.
+  generalize (Int.signed_range n); lia.
 Qed.
 
 Lemma cmpl_ltle_add_one: forall v n,
@@ -593,14 +593,14 @@ Proof.
   intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto.
   unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
   destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by omega. auto.
-  rewrite zlt_true by omega. auto.
+  rewrite zlt_false by lia. auto.
+  rewrite zlt_true by lia. auto.
   rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
   specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)).
   rewrite EQMAX; simpl; intros.
   assert (Int64.signed n <> Int64.max_signed).
   { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); omega.
+  generalize (Int64.signed_range n); lia.
 Qed.
 
 Remark lt_maxsgn_false_int: forall i,
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 97f3ff61..ca0834db 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -13,7 +13,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op RTL ValueDomain.
-Require Import Zbits.
+Require Import Zbits Lia.
 
 (** Value analysis for RISC V operators *)
 
@@ -390,7 +390,7 @@ Proof.
   assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)).
   {
     destruct ob; simpl; auto with va.
-    destruct b; constructor; try omega.
+    destruct b; constructor; try lia.
     change 1 with (usize Int.one). apply is_uns_usize.
     red; intros. apply Int.bits_zero.
   }
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index 5b34dc16..0f303597 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -26,6 +26,7 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL Linking.
+Require Import Lia.
 
 Declare Scope option_monad_scope.
 
@@ -584,8 +585,8 @@ Lemma wellformed_suffix_path c pm path path':
    exists pc', nth_default_succ c (path-path') pc = Some pc' /\ wellformed_path c pm path' pc'.
 Proof.
   induction 1 as [|m].
-  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|omega].
-  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|omega].
+  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|lia].
+  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|lia].
     inversion WF; subst; clear WF; intros; simplify_someHyps.
     intros; simplify_someHyps; eauto.
 Qed.
@@ -602,9 +603,9 @@ Proof.
   intros; exploit fn_path_wf; eauto.
   intro WF.
   set (ps:=path.(psize)).
-  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); omega || eauto.
+  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); lia || eauto.
   destruct 1 as (pc' & NTH_SUCC & WF'); auto.
-  assert (ps - 0 = ps)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - 0 = ps)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst.
   inversion WF'; clear WF'; subst. simplify_someHyps; eauto.
 Qed.
@@ -619,11 +620,11 @@ Lemma internal_node_path path f path0 pc:
 Proof.
   intros; exploit fn_path_wf; eauto.
   set (ps:=path0.(psize)).
-  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { omega. }
+  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { lia. }
   destruct 1 as (pc' & NTH_SUCC & WF').
-  assert (ps - (ps - path) = path)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - (ps - path) = path)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst. 
-  inversion WF'; clear WF'; subst. { omega. }
+  inversion WF'; clear WF'; subst. { lia. }
   simplify_someHyps; eauto.
 Qed.
 
@@ -708,7 +709,7 @@ Proof.
       rewrite CONT. auto.
     + intros; try_simplify_someHyps; try congruence.
       eexists. exists i. exists O; simpl. intuition eauto.
-      omega.
+      lia.
 Qed.
 
 Lemma isteps_resize ge path0 path1 f sp rs m pc st: 
@@ -839,15 +840,15 @@ Lemma stuttering path idx stack f sp rs m pc st t s1':
    RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
    t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m).
 Proof.
-  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto.
+  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); lia || eauto.
   intros (i & pc' & Hi & Hpc & DUM).
   unfold nth_default_succ_inst in Hi.
   erewrite isteps_normal_exit in Hi; eauto.
   exploit istep_complete; congruence || eauto.
   intros (SILENT & st0 & STEP0 & EQ).
   intuition; subst; unfold match_inst_states; simpl.
-  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; omega || eauto.
-  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try omega.
+  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; lia || eauto.
+  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try lia.
   erewrite <- isteps_step_right; eauto.
 Qed.
 
@@ -876,7 +877,7 @@ Proof.
     destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto.
     exists (path0.(psize)); intuition eauto.
     econstructor; eauto.
-    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
     * simpl; eauto.
   + generalize Hi; inversion RSTEP; clear RSTEP; subst; (repeat (simplify_someHyp; simpl in * |- * )); try congruence; eauto.
     - (* Icall *)
@@ -899,7 +900,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
    - (* Ijumptable *)
       intros; exploit exec_Ijumptable; eauto.
@@ -908,7 +909,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
   - (* Ireturn *)
       intros; exploit exec_Ireturn; eauto.
@@ -935,7 +936,7 @@ Proof.
   intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT.
   destruct idx as [ | idx].
   + (* path_step on normal_exit *)
-     assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH.
+     assert (path.(psize)-0=path.(psize))%nat as HH by lia. rewrite HH in PSTEP. clear HH.
      exploit normal_exit; eauto.
      intros (s2' & LSTEP & (idx' & MATCH)).
      exists idx'; exists s2'; intuition eauto.
@@ -944,7 +945,7 @@ Proof.
     unfold match_states; exists idx; exists (State stack f sp pc rs m); 
     intuition.
   + (* one or two path_step on early_exit *)
-    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega.
+    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try lia.
     clear PSTEP; intros PSTEP.
     (* TODO for clarification: move the assert below into a separate lemma *)
     assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0).
@@ -954,7 +955,7 @@ Proof.
       exploit istep_early_exit; eauto.
       intros (X1 & X2 & EARLY_EXIT).
       destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst.
-      exploit (internal_node_path path0); omega || eauto.
+      exploit (internal_node_path path0); lia || eauto.
       intros (i' & pc' & Hi' & Hpc' & ENTRY).
       unfold nth_default_succ_inst in Hi'.
       erewrite isteps_normal_exit in Hi'; eauto.
@@ -976,8 +977,8 @@ Proof.
       - simpl; eauto.
     * (* single step case *)
       exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto.
-      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega.  simpl; eauto. }
-      - omega.
+      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try lia.  simpl; eauto. }
+      - lia.
       - simpl; eauto.
       - simpl; eauto.
       - intuition subst.
@@ -1002,7 +1003,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
   + (* exec_function_external *)
     destruct f; simpl in H3 |-; inversion H3; subst; clear H3.
@@ -1021,7 +1022,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
 Qed.
 
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index c6a4d409..21f89f90 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -7,6 +7,7 @@ Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -668,7 +669,7 @@ Proof.
   induction l2.
   - intro. destruct l1; auto. apply is_tail_false in H. contradiction.
   - intros ITAIL. inv ITAIL; auto.
-    apply IHl2 in H1. clear IHl2. simpl. omega.
+    apply IHl2 in H1. clear IHl2. simpl. lia.
 Qed.
 
 Lemma is_tail_nth_error {A} (l1 l2: list A) x:
@@ -678,14 +679,14 @@ Proof.
   induction l2.
   - intro ITAIL. apply is_tail_false in ITAIL. contradiction.
   - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H.
-    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H.
+    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; lia). rewrite H. clear H.
     inv ITAIL.
-    + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H.
+    + assert (forall n, (n - n)%nat = 0%nat) by (intro; lia). rewrite H.
       simpl. reflexivity.
     + exploit IHl2; eauto. intros. clear IHl2.
-      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega).
+      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; lia).
       exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
-      assert ((length l2 > length l1)%nat) by omega. clear H2.
+      assert ((length l2 > length l1)%nat) by lia. clear H2.
       rewrite H0; auto.
 Qed.
 
diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
index 404c2a96..c8eadbd7 100644
--- a/scheduling/postpass_lib/Machblock.v
+++ b/scheduling/postpass_lib/Machblock.v
@@ -29,6 +29,7 @@ Require Import Conventions.
 Require Stacklayout.
 Require Import Mach.
 Require Import Linking.
+Require Import Lia.
 
 (** * Abstract Syntax *)
 
@@ -87,9 +88,9 @@ Lemma size_null b:
 Proof.
   destruct b as [h b e]. cbn. unfold size. cbn.
   intros H.
-  assert (length h = 0%nat) as Hh; [ omega |].
-  assert (length b = 0%nat) as Hb; [ omega |].
-  assert (length_opt e = 0%nat) as He; [ omega|].
+  assert (length h = 0%nat) as Hh; [ lia |].
+  assert (length b = 0%nat) as Hb; [ lia |].
+  assert (length_opt e = 0%nat) as He; [ lia|].
   repeat split.
   destruct h; try (cbn in Hh; discriminate); auto.
   destruct b; try (cbn in Hb; discriminate); auto.
diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
index d121a54b..1d6c6e18 100644
--- a/scheduling/postpass_lib/Machblockgenproof.v
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -30,6 +30,7 @@ Require Import Linking.
 Require Import Machblock.
 Require Import Machblockgen.
 Require Import ForwardSimulationBlock.
+Require Import Lia.
 
 Ltac subst_is_trans_code H :=
   rewrite is_trans_code_inv in H;
@@ -318,12 +319,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe
 
 Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
 Proof.
-  unfold add_label, size; cbn; omega.
+  unfold add_label, size; cbn; lia.
 Qed.
 
 Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1.
 Proof.
-  intro H. unfold add_basic, size; rewrite H; cbn. omega.
+  intro H. unfold add_basic, size; rewrite H; cbn. lia.
 Qed.
 
 
@@ -341,13 +342,13 @@ Proof.
   remember (trans_code (i::c)) as bl.
   rewrite <- is_trans_code_inv in Heqbl.
   inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl.
-  - rewrite size_add_to_newblock; omega.
+  - rewrite size_add_to_newblock; lia.
   - rewrite size_add_label;
     subst_is_trans_code H.
-    omega.
+    lia.
   - rewrite size_add_basic; auto.
     subst_is_trans_code H. 
-    omega.
+    lia.
 Qed.
 
 Local Hint Resolve dist_end_block_code_simu_mid_block: core.
@@ -357,9 +358,9 @@ Lemma size_nonzero c b bl:
   is_trans_code c (b :: bl) -> size b <> 0.
 Proof.
    intros H; inversion H; subst.
-   - rewrite size_add_to_newblock; omega.
-   - rewrite size_add_label; omega.
-   - rewrite size_add_basic; auto; omega.
+   - rewrite size_add_to_newblock; lia.
+   - rewrite size_add_label; lia.
+   - rewrite size_add_basic; auto; lia.
 Qed.
 
 Inductive is_header: list label -> Mach.code -> Mach.code -> Prop :=
@@ -633,7 +634,7 @@ Proof.
       unfold dist_end_block_code. 
       subst_is_trans_code Heqtc.
       lapply (size_nonzero c b bl); auto.
-      omega.
+      lia.
     }
     rewrite X in H; unfold size in H.
     (* decomposition of starN in 3 parts: header + body + exit *)
@@ -697,7 +698,7 @@ Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)
   - intros s1 t s1' H1 H2.
-    destruct H1; cbn in * |- *; omega || (intuition auto);
+    destruct H1; cbn in * |- *; lia || (intuition auto);
     destruct H2; eapply cfi_dist_end_block; cbn; eauto.
 (* public_preserved *)
   - apply senv_preserved.