Commit 2024-04-16 22:37 8f9698de

feat(Order): limit elements in well-ordered types (#11584) This PR introduces two main definitions:

• wellOrderSucc a: the successor of an element a in a well-ordered type
• the typeclass IsWellOrderLimitElement a which asserts that an element a (in a well-ordered type) is neither a successor nor the smallest element, i.e. a is a limit element Then, the lemma eq_bot_or_eq_succ_or_isWellOrderLimitElement shows that an element in a well-ordered type is either ⊥, a successor, or a limit element.