import scas.base.
import scas.polynomial.tree.SolvablePolynomial
import .given

val r = SolvablePolynomial.weylAlgebra()("a", "x", "b", "y")
val axby = r.generators
import r.given

assert (b * a + y * x >< 2abxy)
assert (r == axby1abba1xyyx)