--- a/src/MoreDep.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/MoreDep.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import Arith Bool List Omega.
+Require Import Arith Bool List Lia.
 
 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
 
@@ -871,6 +871,7 @@
 (* end hide *)
 
 (** A few auxiliary functions help us in our final matcher definition.  The function [split] will be used to implement the regexp concatenation case. *)
+Hint Extern 1 (_ <= _) => lia.
 
 Section split.
   Variables P1 P2 : string -> Prop.
@@ -938,7 +939,7 @@
   induction s; substring.
 Qed.
 
-Hint Rewrite substring_self substring_empty using omega.
+Hint Rewrite substring_self substring_empty using lia.
 
 Lemma substring_split' : forall s n m,
   substring n m s ++ substring (n + m) (length s - (n + m)) s
@@ -986,7 +987,7 @@
       | [ |- ?N >= _ ] => destruct N; crush
     end;
     match goal with
-      [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
+      [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | lia ]
     end.
 Qed.
 
@@ -998,19 +999,19 @@
 Qed.
 
 Hint Rewrite substring_stack substring_stack' substring_suffix
-  using omega.
+  using lia.
 
 Lemma minus_minus : forall n m1 m2,
   m1 + m2 <= n
   -> n - m1 - m2 = n - (m1 + m2).
-  intros; omega.
+  intros; lia.
 Qed.
 
 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
-  intros; omega.
+  intros; lia.
 Qed.
 
-Hint Rewrite minus_minus using omega.
+Hint Rewrite minus_minus using lia.
 (* end hide *)
 
 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *)
@@ -1099,7 +1100,8 @@
     (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *)
 
     (** Now we come to [dec_star''] itself.  It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split'].  The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *)
-
+    Hint Extern 2 (_ \/ _) => lia.
+    
     Definition dec_star'' : forall l : nat,
       {exists l', S l' <= l
         /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}