pred (predecessor)
predecessor of this element in an enumerated type
letting D be new type enum { North, East, South, West }
find a : D such that a = pred(East) $North
This result shows a
must be the predecessor of East
.
See it demonstrated here.