diff options
| author | Vincent Laporte | 2019-10-28 12:54:01 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:38 +0000 |
| commit | b3fc3cbd36570b77af9f17237f30713be861c3ed (patch) | |
| tree | 825a1b321d6fc12c5124d7b36029342d83601831 /plugins/nsatz | |
| parent | e0e52b72b532b5e487067750b8d860fc2df10df6 (diff) | |
Nsatz: use “lia” rather than “omega”
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 8 |
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. |