This file defines two notions of sorted list:
- a list is locally sorted if any element is smaller or equal than
its successor in the list
- a list is sorted if any element coming before another one is
smaller or equal than this other element
The two notions are equivalent if the order is transitive.