diff options
| author | Vincent Laporte | 2019-10-28 12:52:51 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-31 21:51:09 +0000 |
| commit | 87e2bd27055db7827ab5d5a677e3c6fc876685c6 (patch) | |
| tree | 1298045a7a75af8014eb35a65862b44a3659538b /plugins | |
| parent | 82461ff590360a1223fad69446b77f535d28b6b4 (diff) | |
lra: use “lia” rather than “omega”
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/RMicromega.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 3651b54ed8..6c1852acbf 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -22,6 +22,7 @@ Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. +Require Import Lia. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -192,7 +193,7 @@ Proof. destruct z ; try congruence. compute. congruence. compute. congruence. - generalize (Zle_0_nat n). auto with zarith. + generalize (Zle_0_nat n). auto using Z.le_ge. Qed. Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1). @@ -333,7 +334,7 @@ Proof. apply Qeq_bool_eq in C2. rewrite C2. simpl. - rewrite Qpower0 by auto with zarith. + rewrite Qpower0 by lia. apply Q2R_0. + rewrite Q2RpowerRZ. rewrite IHc. @@ -341,7 +342,7 @@ Proof. rewrite andb_false_iff in C. destruct C. simpl. apply Z.ltb_ge in H. - auto with zarith. + lia. left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. |