True exact I. Qed.
The first exercise:
Get a root of the polynomial x**3 + 3*x**2 + 4*x + 2 0 using z3. Can you use z3 to show this is the only solution?
Here we open up the reals.
It is easy enough to confirm that the solution of x -1 is a zero using the [ring] tactic.
Require Import Reals.
Open Scope R_scope.
Print Scope R_scope.
Scope R_scope
Delimiting key is R
Bound to class R
"r ²" : Rsqr r
"x ^ y" : pow x y
"x y" : Rge x y
"x y" : Rgt x y
"x y z" : and (Rle x y) (Rle y z)