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/rexample.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite/micromega/rexample.v') diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index d7386a4e..9bb9dacc 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -12,7 +12,7 @@ Require Import Ring_normalize. Open Scope R_scope. -Lemma yplus_minus : forall x y, +Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -34,7 +34,7 @@ Proof. Qed. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : R) (m : R) (jt : R) @@ -64,12 +64,12 @@ Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. Proof. intros. - psatz R 2. + psatz R 3. Qed. Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 ) *x^2*y^2) >= 0. Proof. - intros ; psatz R. + intros ; psatz R 2. Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -- cgit v1.2.3