diff options
Diffstat (limited to 'test-suite/micromega/qexample.v')
| -rw-r--r-- | test-suite/micromega/qexample.v | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 42aff5a4..1fa250e0 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -6,7 +6,7 @@ (* *) (************************************************************************) -Require Import Micromegatac. +Require Import Psatz. Require Import QArith. Require Import Ring_normalize. @@ -14,22 +14,25 @@ Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. - omicron Q. + psatzl Q. Qed. + + + (* Other (simple) examples *) Open Scope Q_scope. Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2). Proof. intros. - omicron Q. + psatzl Q. Qed. Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m. Proof. - intros ; omicron Q. + intros ; psatzl Q. Qed. Open Scope Z_scope. Open Scope Q_scope. @@ -58,5 +61,19 @@ Lemma vcgen_25 : forall (( 1# 1) == (-2 # 1) * i + it). Proof. intros. - omicron Q. + psatzl Q. +Qed. + +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +Proof. + intros. + psatz Q 2. 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. +Qed. + + + |