From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/micromega/qexample.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite/micromega/qexample.v') 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. -- cgit v1.2.3