使用例

　まずは，各*proveの違いを確認します．proveは，a,b,cを

prove(a+b>=c);
The inequality holds.

のように１つの３角形の３辺の長さと見な做します．xproveでは

xprove(a+b>=c);
output a counter-example
[1/4, 1/2, 1]
The inequality does not hold.

xprove(v>=0);
The inequality holds.
true

のように各変数を非負値と見做し，sproveも同様ですが

sprove(u+v>=0);
Doing Difference Substitution ...
This is trivial by Difference Substitution
The inequality holds.

のように対称多項式用のアルゴリズムを用い，その他の入力に対しては

sprove(2*u+v>=0);
Warning: the expression is not symmetric!
...
　
sprove(u+1/sqrt(v)>=0)
Warning: not a polynomial inequality, which will be verified by xprove( )
...

のようにxproveを呼びます．そして，yproveは

yprove(v>=0);
output a counter example
[v = -1]
The inequality does not hold.

yprove(v^2>=0);
The inequality holds!

のように各変数を実数値と見做すだけです．
　例を挙げます．

prove( a^2+b^2+c^2 <= 2 (a*b+b*c+c*a) );
The inequality holds, 53.773

このproveは

a:=x+y,b:=y+z,c:=z+x

により非負値変数に変換して次のxproveを呼ぶもので，３角比は余弦定理を利用しています．従って

prove(a>=b,[cos(A)>=cos(B)]);
The inequality inversely holds.

となりますが，角度のみでは

prove(a>=b,[A>=B]);
output a counter-example
[2, 1, 3, 1/2]
The inequality does not hold.

のように失敗します．一方，半角公式は組み込まれているので

prove(sin(A)+sin(B)+sin(C/2)<=sqrt(5));
The original inequality is equivalent to the following inequalities:
...
The inequality holds !

と答えてくれます．また，このsqrt(5)がクリティカルであることを確かめるには，cminが使えます．

cmin(sin(A)+sin(B)+sin(C/2)<=t,[],t);
...
The best possible minimal const t is a root of the following polynomial :
t^2-5
which is between 11/5,3

なお，Mathematicaは

Reduce[ForAll[{A, B, C}, A + B + C == Pi && A > 0 && B > 0 && C > 0,
Sin[A] + Sin[B] + Sin[C/2] <= k], Reals]

としてもお手上げと答えるのみです．
　次は高さh＊，内角の２等分線の長さw＊，中線の長さm＊，周の長さの半分sについての関係です．

prove( ha+wb+mc < = sqrt(3) s );
The original inequality is equivalent to the following inequalities:
...
The inequality holds !

w＊は内角２等分線の長さ，r＊は傍接円の半径の長さ
でした．

prove( wa/ra+wb/rb+wc/rc >= 3 (wa+wb+wc)/(ha+hb+hc) );
...
The inequality holds, 12066.895

　xproveでは全ての変数は非負値と見て処理されます．

xprove( (a+b+c+1/sqrt(d)) (1/a+1/b+1/c+sqrt(d)) > = 16 );
The inequality holds !
true

　次は少し難しい例です．

xprove( (a + b + c) (1/a + 1/b + 1/c) > = 9 + 5 2^(-3/5) ( (1 - a/b) (1 - b/c) (1 - c/a) ) ^ ( 4/5 ) );
...

入力は瞬時に多項式への変換されますが，そこから先に進みませんので

sprove(30760 a^8 b^4 c^3 + ... + 40 a^10 c b^4>=0);
Doing Difference Substitution
...
The inequality holds, 389.222

のように対称式用のsproveの出番となります．