%use(int).
%X=<Y -> s(X)=<s(Y).
s(X)<s(Y) -> X<Y.
s(X)=<s(Y) -> X=<Y.
%X<Y -> s(X)=<Y.
0<X -> s(p(X))=X.