Conditionally complete and canonically ordered

Stream: Is there code for X?

[Brendan Seamas Murphy]

If I assume both [ConditionallyCompleteLinearOrder α] and [CanonicallyLinearOrderedAddCommMonoid α] I end up with two distinct orders on α, yes? Is there a way to assume that α is both conditionally complete and is canonically ordered? My understanding is no, and that the reason these types aren't mixins is because we want to use custom values of min/max/sup/inf. Is there a way to assume both of these things in mathlib as-is?

[Yuyang Zhao]

There has been a plan to make ordered algebraic typeclasses into mixins. See #13519.