Merge PR #11076: Remove all remaining calls to “omega” from the standard library

Reviewed-by: ejgallego

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 58d01c125c..896ee303cc 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -31,6 +31,7 @@ Require Export Ncring_tac.
 Require Export Integral_domain.
 Require Import DiscrR.
 Require Import ZArith.
+Require Import Lia.
 
 Declare ML Module "nsatz_plugin".
 
@@ -413,7 +414,7 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
             try exact integral_domain_minus_one_zero
           || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
                      one, one_notation, multiplication, mul_notation, zero, zero_notation;
-                     discrR || omega]) 
+                     discrR || lia ])
           || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]
@@ -502,7 +503,7 @@ reflexivity. exact Qplus_opp_r.
 Defined.
 
 Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-unfold Qeq. simpl. auto with *. Qed.
+Proof. unfold Qeq. simpl. lia.  Qed.
 
 Instance Qcri: (Cring (Rr:=Qri)).
 red. exact Qmult_comm. Defined.
@@ -513,8 +514,7 @@ exact Qmult_integral. exact Q_one_zero. Defined.
 
 (* Integers *)
 Lemma Z_one_zero: 1%Z <> 0%Z.
-omega. 
-Qed.
+Proof. lia. Qed.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.