Missing order stuff

Stream: general

[Yaël Dillies]

As you may have seen, I'm currently roaming the order library in search of missing instances. Here's my current kill list:

• Disjoint order on sigma types and its locally finite order instance
• Locally finite order instance for sum
• Locally finite order instance on lexicographical prod.
• Order on tree and its locally finite order instance
• Prefix order on list and its locally finite order instance

Along with other people, I'm also defining some more order typeclasses and concepts:

• Minimal elements (#11268)
• Locally listable orders (currently branch#fin_range)
• Graded orders (#11308)
• Diamond orders (branch#polytopes)
• Abstract polytopes (branch#polytopes)
• Sperner orders
• Incidence algebras (branch#incidence_algebra)
• Eulerian orders

If there's any more you want to see, please send it here!