--- a/src/GeneralRec.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/GeneralRec.v	Sun Jul 31 14:48:22 2022 -0400
@@ -8,7 +8,7 @@
  *)
 
 (* begin hide *)
-Require Import Arith List Omega.
+Require Import Arith List Lia.
 
 Require Import Cpdt.CpdtTactics Cpdt.Coinductive.
 
@@ -163,7 +163,9 @@
   (** We must prove that the relation is truly well-founded.  To save some space in the rest of this chapter, we skip right to nice, automated proof scripts, though we postpone introducing the principles behind such scripts to Part III of the book.  Curious readers may still replace semicolons with periods and newlines to step through these scripts interactively. *)
 
   Hint Constructors Acc.
-
+  Hint Extern 2 (Acc _ _) => lia.
+  Hint Extern 2 (_ <= _) => lia.
+  
   Lemma lengthOrder_wf' : forall len, forall ls, length ls <= len -> Acc lengthOrder ls.
     unfold lengthOrder; induction len; crush.
   Defined.
@@ -506,7 +508,7 @@
 
   (** Now it is straightforward to package [Fix'] as a computation combinator [Fix]. *)
 
-  Hint Extern 1 (_ >= _) => omega.
+  Hint Extern 1 (_ >= _) => lia.
   Hint Unfold leq.
 
   Lemma Fix'_ok : forall steps n x v, proj1_sig (Fix' n x) steps = Some v