diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_3652.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_3652.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v index 915cfcac27..b21a4d939c 100644 --- a/test-suite/bugs/closed/bug_3652.v +++ b/test-suite/bugs/closed/bug_3652.v @@ -1,6 +1,7 @@ Require Setoid. Require ZArith. Import ZArith. +Require Import Lia. Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A. @@ -87,12 +88,12 @@ Proof. unfold zotval. unfold mp2a1s. ring_simplify'. - replace 2 with (2*1) at 2 7 by omega. + replace 2 with (2*1) at 2 7 by lia. rewrite <-?Z.mul_assoc. rewrite <-?Z.mul_add_distr_l. rewrite <-Z.mul_sub_distr_l. - rewrite Z.mul_cancel_l by omega. - replace 1 with (2-1) at 1 by omega. + rewrite Z.mul_cancel_l by lia. + replace 1 with (2-1) at 1 by lia. rewrite Z.add_sub_assoc. rewrite Z.sub_cancel_r. Unshelve. |