diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/micromega/qexample.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/micromega/qexample.v')
| -rw-r--r-- | test-suite/micromega/qexample.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 1fa250e0..76dc52e6 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -10,7 +10,7 @@ Require Import Psatz. Require Import QArith. Require Import Ring_normalize. -Lemma plus_minus : forall x y, +Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. @@ -37,7 +37,7 @@ Qed. Open Scope Z_scope. Open Scope Q_scope. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : Q) (m : Q) (jt : Q) @@ -67,12 +67,12 @@ Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. Proof. intros. - psatz Q 2. + psatz Q 3. Qed. Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 # 1) *x^2*y^2) >= 0. Proof. - intros ; psatz Q. + intros ; psatz Q 3. Qed. |