Commit 2024-09-12 05:45 6bdc3635

feat(SetTheory/Ordinal/Basic): prove linear order instance earlier (#16401) We show that for any two well-orders, one is an initial segment of the other, without relying on ordinal addition or anything of the sort. By doing this, we can move the LinearOrder instance on ordinals right next to the partial order one.