/*
dense total orderings without endpoints
*/

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

% reflexive_closure

X=<X.
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.