mathlib3

5abbfc93 - feat(logic/equiv/fin): `succ_above` as an equivalence (#16278)

feat(logic/equiv/fin): `succ_above` as an equivalence (#16278) Add a version of `succ_above` that's a bundled order isomorphism between `fin n` and `{x : fin (n + 1) // x ≠ p}`.