Prune spurious roots in lazard evaluation of coverings solver (#8200)

Prune spurious roots in lazard evaluation of coverings solver (#8200)

This PR fixes a subtle issue in the Lazard evaluation used in the coverings solver if --nl-cov-lift=lazard is used.
When isolating real roots (over a partial assignment that contains real algebraic number), the core root solver may find roots that are spurious, i.e., they are not actually roots of the input polynomial. This is due to the way how the multivariate polynomial is "partially evaluated" before calling the univariate real root isolation.
When using the libpoly real root isolation, this is all done internally. For the Lazard evaluation, however, we explicitly call the libpoly real root isolation on a univariate polynomial that already has these spurious roots, hence we need to remove them ourselves.

While debugging this issue, another weird oversight was detected (and fixed): for some reason we expected the vanishing factor (after factoring the defining polynomial when constructing the next field extension) to only have two term. There is no reason for this restriction, and the code below works just fine.