Groebner.jl is useful for solving a system of polynomial equations. This is about a method of transforming an inequality into an equation, so it could be used with Groebner.jl.

Suppose, for example, I have this simple equation: {\left(x-2\right) \cdot \left(x+3\right)} = 0. It has two solutions, 2 and -3. Now suppose we had this equation in a system together with the inequality 0 \le x. Now there’s only a single solution, 2, because -3 is negative.

To make the above system usable in Groebner.jl, the inequality must be turned into a set of equations. Luckily, I thought, this should be easy: 0 \le x should be equivalent with x = {y^2}, where y is a newly introduced variable, because a square is never negative. Supposing both x and y are real, that is.

This is why I hoped that if I input the equations {\left(x-2\right) \cdot \left(x+3\right)} = 0 and x = {y^2} into `Groebner.groebner`

, I would get a system containing the equation {x-2}=0 as output. This is, however, not the case - Groebner.jl doesn’t seem to be able to eliminate the negative solution. I guess perhaps Groebner.jl doesn’t know that I intend for the variables to be real?

I’m wondering why is that, is it a limitation inherent in the algorithm, and is there another way to solve inequalities with Groebner.jl.

REPL example:

```
julia> using DynamicPolynomials, Groebner
julia> @polyvar x y
(x, y)
julia> groebner([(x - 2)*(x + 3), x - y^2])
2-element Vector{Polynomial{DynamicPolynomials.Commutative{DynamicPolynomials.CreationOrder}, Graded{LexOrder}, Int64}}:
-x + y²
-6 + x + x²
```

EDIT: here’s another example, I would expect the output here to be 0 = 1 (“inconsistent system”):

```
julia> groebner([(x + 2)*(x + 3), x - y^2])
2-element Vector{Polynomial{DynamicPolynomials.Commutative{DynamicPolynomials.CreationOrder}, Graded{LexOrder}, Int64}}:
-x + y²
6 + 5x + x²
```

@sumiya11 hope you can give some insight