Commit 2026-06-09 16:55 97d811a4

feat(Order/SuccPred/CompleteLinearOrder): generalize csSup_mem_of_not_isSuccLimit (#38142) Given s.Nonempty and BddAbove s we can conclude sSup s ∈ s using either:

• csSup_mem_of_not_isSuccPrelimit, given ConditionallyCompleteLinearOrder and ¬IsSuccPrelimit (sSup s)
• csSup_mem_of_not_isSuccLimit, given ConditionallyCompleteLinearOrderBot and ¬IsSuccLimit (sSup s) We generalize both to a theorem that requires ConditionallyCompleteLinearOrder and ¬IsSuccLimit (sSup s). This creates 8 theorems that require ¬IsSuccPrelimit but are now easily proved with the ¬IsSuccLimit theorems, we replace csSup_mem_of_not_isSuccPrelimit/exists_eq_ciSup_of_not_isSuccPrelimit with their primed ConditionallyCompleteLinearOrderBot theorems, and deprecates the other 6. Tags a random to_dual (in ConditionallyCompleteLattice/Basic.lean) to let us to_dualize the new lemmas.