Define a ring of polynomials. The order of variables is z > y > x.
Define a set of linear equations and inequalities.
We eliminate variables according to the order z > y > x.
The output is a set of equivalent linear equations and inequalities sorted in ascending order according to the largest variables appearing in the constraints. It provides conditions on lower order variables such that higher order variables have solutions.
Now compute the projection of sys.
The output is a set of linear constraints describing the projection of the zero set of sys onto space.
The option 'canonical' can be used to remove redundancies among constraints having the same main variables.