use(ag).

X*Y = Y*X.


(q(X)+ (-q(Y))) = (X+Y)*(X+ (-Y)).

X<X -> [].
X<Y, Y<Z -> X<Z.
X<Y, Y=<X.

0<Z => ((X*Z < Y*Z)==(X < Y)).
X<Y -> X+Z < Y+Z.


goal
~ forall(A, forall(B, 0=<A and 0=<B => ((q(A)+(-q(B))=<0) == ((A+(-B))=<0)))).

precedence([q,*,-,+]).

%option(search_depth(0)).

/*



*/