mathlib3

a08d1797 - refactor(set_theory/ordinal/*): `ordinal.succ` → `order.succ` (#14243)

refactor(set_theory/ordinal/*): `ordinal.succ` → `order.succ` (#14243) We inline the definition of `ordinal.succ` in the `succ_order` instance. This allows us to comfortably use all of the theorems about `order.succ` to our advantage.