Document new order classes

What question should the reference manual answer?

How should I implement orderings for my type?

Additional context

The system of ordering relations was recently revamped, and should be documented.

The overall description is in this thread, and I got these further details to add:

Most order-related stuff can be found in Init.Data.Order.

Lemmas about linear orders are not required to require all the basic operations (like LE, LT, Ord, BEq, Min and so on). The need to require LE and IsLinearOrder, and for each additional operation X, LawfulOrderX. How this plays out for max?_eq_some_iff can be seen in the linked post.

Assume that you are writing a lemma about a linear order and only want to require LE. It is possible to use lemmas requiring more operations: Opening Classical.Order activates default instances for the operations, derived from LE. For example, the OrientedOrd instance in Init.Data.Order.Lemmas, which does not mention LT, can rely on the lemma compare_eq_lt [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α] {a b : α} : compare a b = .lt ↔ a < b.

Start with Init.Data.Order and the linked Zulip feedback thread to understand the revamped ordering relations and their required operations. Document how to implement orderings for a type, including the LE and IsLinearOrder requirements, LawfulOrderX classes, and Classical.Order defaults. Done means the reference manual answers the stated implementation question and covers these details.