--- a/src/CpdtTactics.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/CpdtTactics.v	Sun Jul 31 14:48:22 2022 -0400
@@ -7,7 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-Require Import Eqdep List Omega.
+Require Import Eqdep List Lia.
 
 Set Implicit Arguments.
 
@@ -196,8 +196,8 @@
           repeat (simplHyp invOne; intuition)); un_done
       end;
       sintuition; rewriter; sintuition;
-      (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
-      try omega; try (elimtype False; omega)).
+      (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *)
+      try lia; try (elimtype False; lia)).
 
 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
 Ltac crush := crush' false fail.