diff options
Diffstat (limited to 'test-suite/micromega/rexample.v')
| -rw-r--r-- | test-suite/micromega/rexample.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 1de1955db..d7386a4ec 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -69,7 +69,7 @@ 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 ; sos R. + intros ; psatz R. Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). |