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.