diff options
Diffstat (limited to 'doc/refman/Micromega.tex')
| -rw-r--r-- | doc/refman/Micromega.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index a43cd15b0..2fe7c2f7f 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -96,9 +96,9 @@ To illustrate the working of the tactic, consider we wish to prove the following Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. \end{coq_example*} \begin{coq_eval} -intro x; psatz Z. +intro x; psatz Z 2. \end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z}. The oracle returns the cone expression $2 \times +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the cone expression $2 \times (\mathbf{x-1}) + \mathbf{x-1}\times\mathbf{x-1} + \mathbf{-x^2}$ (polynomial hypotheses are printed in bold). By construction, this expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By Theorem~\ref{thm:psatz}, the goal is valid. |