succ (successor)

successor of this element in an enumerated type

letting D be new type enum { North, East, South, West }
find a : D such that a = succ(South) $West

This result West shows a must be the successor of South.

See it demonstrated here.