/*

*/


% total ordering
X<Y, Y<Z -> X<Z.
X<X -> [].
X<Y, Y<X, X=Y.

% reflexive_closure

X<Y -> X=<Y.
X=<Y -> X=Y,X<Y.

% density
X<Y -> X<d(X,Y).
X<Y -> d(X,Y)<Y.

% no endpoints
X<n(X).
p(X)<X.