diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 17:39:58 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 17:39:58 +0000 |
| commit | 3e6d3a9a35660e32c478ac8e5da5e76d25c905b5 (patch) | |
| tree | 8015d66f8df3fea6efa3c561ebacf5a42df81d14 /test-suite/micromega/square.v | |
| parent | 3c75aed311c024cc35c1690d7bfec5c88140457e (diff) | |
Minor fixes in the test-suite after my recent commits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/micromega/square.v')
| -rw-r--r-- | test-suite/micromega/square.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 6fa547358..8767f6874 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -9,11 +9,11 @@ Require Import ZArith Zwf Psatz QArith. Open Scope Z_scope. -Lemma Z.abs_square : forall x, (Z.abs x)^2 = x^2. +Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. intros ; case (Zabs_dec x) ; intros ; psatz Z 2. Qed. -Hint Resolve Z.abs_nonneg Z.abs_square. +Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. |