About eliminate(...)

This post is motivated by a recent answer where I needed a necessary and sufficient condition for three straight lines in space be concurrent. I had to use determinants because the eliminate command did not provide the correct answer.
Investigating the cause, I saw that eliminate uses an heuristic algorithm, instead of using Groebner bases (when possible).

Here is an example.

We want to eliminate the unknowns x an y in the system

a*x + y = 0,  b*x+y+1 = 0, c*x+2*y = 0

So, apparently, the elimination is not possible, i.e. for each triple (a,b,c), the system in x and y is incompatible.
This is not true. For example,

eliminate  obtained its result this way (just like a superficial human):

Now, the correct result (also by hand):

So, for c = 2*a  (and a <> b)  the system in x,y  is compatible.

This result can be obtained with Groebner bases.

Note that it is more efficient to use lexdeg([x,y], [a,b,c])  instead of plex(x,y,a,b,c).

The conclusion is that eliminate should use internally Groebner:-Basis for polynomial systems.
Until then, we can use it ourselves!