Tracking issue: Ordinal refactors

[vihdzp]

This issue keeps track of various miscellaneous planned refactors to the Ordinal part of the library, mostly cleaning up definitions that should be replaced with more general concepts.

• Deprecate Ordinal.sup: [Merged by Bors] - refactor(SetTheory/Ordinal/Arithmetic): Ditch Ordinal.sup #15820
• Deprecate Ordinal.bsup
• Deprecate Ordinal.lsub and Ordinal.blsub
• Deprecate Ordinal.blsub₂: [Merged by Bors] - refactor(SetTheory/Ordinal/Arithmetic): deprecate blsub₂ #17679
• Deprecate Ordinal.mex and Ordinal.bmex: [Merged by Bors] - chore(SetTheory/Ordinal/Arithmetic): deprecate Ordinal.mex and Ordinal.bmex #16989
• Deprecate the BFamily API
• Change Set.Unbounded (· < ·) to ¬ BddAbove: [Merged by Bors] - refactor(SetTheory/Ordinal/Enum): better definition for Ordinal.enumOrd #16962
• Replace Ordinal.IsLimit by Order.IsSuccLimit
• Replace Order.succ x by x + 1

Some bonus stuff which probably needs to be discussed beforehand.

• Replace Ordinal.nfp by OmegaCompletePartialOrder.fixedPoints.iterateChain
• Redefine Cardinal.univ in terms of #Cardinal: refactor(SetTheory/*/Univ): redefine Cardinal.univ #17969
• Generalize Ordinal.pred to preorders