Unbundled relations and ordinal API

Stream: mathlib4

[Violeta Hernández]

For the longest time I've always found the usage of unbundled relations in the docs#Ordinal API to be quite annoying. Mathematically, ordinals are supposed to be equivalence classes of well-orders, but in practice we can't use this characterization very well because the API is stated in the setting of IsWellOrder α r, rather than LinearOrder α + WellFoundedLT α. And this leads to bespoke theorems like docs#Ordinal.bounded_singleton or docs#Cardinal.unbounded_of_unbounded_sUnion which are hard to even parse.

I would like to change the API to one taking bundled well-orders, rather than unbundled ones. I've already taken a first step towards this in #35513, which redefines docs#Order.cof to take in a preorder rather than a reflexive relation, which allows us to use the existing API on docs#IsCofinal (the changed proofs are much nicer now, in my opinion). But my intention is to eventually redefine even ordinals themselves, as a quotient of a type of bundled well-orders, rather than a type of unbundled ones.

I see one potential problem with this: we might want to, under some circumstances, define a well-order on a type that already has an order instance. It's not unheard of to see mathematical arguments start with sentences such as "take a well-ordering of the reals". Though I'd argue that this could be dealt with via a type alias, perhaps something like WellOrder α, which overrides any order structure on α and declares its own LinearOrder + WellFoundedLT instances.

I'm mostly just opening this thread as a sanity check that what I'm doing is desirable, and that no one has any major complaints about the new design.

cc. @Yan Yablonovskiy 🇺🇦 @Snir Broshi @Yaël Dillies

[Yan Yablonovskiy 🇺🇦]

@Bhavik Mehta you may also be interested in this , as it touches on your idea for the ordinal/order type refactor.