mathlib

ce0dc836 - feat(set_theory/ordinal/basic): Supremum indexed over an empty / unique type (#13735)

feat(set_theory/ordinal/basic): Supremum indexed over an empty / unique type (#13735) This PR contains the following changes: - The lemmas `sup_unique`, `bsup_one`, `lsub_unique`, `blsub_one`. - `congr` lemmas for `bsup` and `blsub` - Arguments like `o = 0` are removed as the `congr` lemmas now handle this. - `a + 1` is changed to `a.succ` in some lemmas (for better rewriting).