mathlib

b67857e7 - refactor(set_theory/ordinal_arithmetic): Reworked `sup` and `bsup` API (#11048)

refactor(set_theory/ordinal_arithmetic): Reworked `sup` and `bsup` API (#11048) This PR does two things: - It reworks and matches, for the most part, the API for `ordinal.sup` and `ordinal.bsup`. - It introduces `ordinal.lsub` and `ordinal.blsub` for (bounded) least strict upper bounds, and proves the expected results.