diff options
Diffstat (limited to 'test-suite/micromega/qexample.v')
| -rw-r--r-- | test-suite/micromega/qexample.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index c9c779f90..76dc52e6c 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -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. |