feat: generalize IsSuccLimit.bot_lt to preorders (leanprover-community#38237)

Author: vihdzp

Mathlib/Order/BoundedOrder/Basic.lean

@@ -122,6 +122,15 @@ theorem ne_top_of_lt (h : a < b) : a ≠ ⊤ :=
 
 @[to_dual bot_lt] alias LT.lt.lt_top := lt_top_of_lt
 
+@[to_dual bot_lt_iff_not_le_bot]
+theorem lt_top_iff_not_top_le : a < ⊤ ↔ ¬ ⊤ ≤ a := by
+  simp [lt_iff_le_not_ge]
+
+@[to_dual not_isMin_iff_bot_lt]
+theorem not_isMax_iff_lt_top : ¬ IsMax a ↔ a < ⊤ := by
+  rw [not_isMax_iff]
+  exact ⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩
+
 attribute [aesop (rule_sets := [finiteness]) unsafe 20%] ne_top_of_lt
 -- would have been better to implement this as a "safe" "forward" rule, why doesn't this work?
 -- attribute [aesop (rule_sets := [finiteness]) safe forward] ne_top_of_lt

Mathlib/Order/SuccPred/Limit.lean

@@ -147,9 +147,12 @@ theorem not_isSuccLimit_bot [OrderBot α] : ¬ IsSuccLimit (⊥ : α) :=
   isMin_bot.not_isSuccLimit
 
 @[to_dual]
-theorem IsSuccLimit.ne_bot [OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥ := by
-  rintro rfl
-  exact not_isSuccLimit_bot h
+theorem IsSuccLimit.bot_lt [OrderBot α] (h : IsSuccLimit a) : ⊥ < a :=
+  not_isMin_iff_bot_lt.1 h.not_isMin
+
+@[to_dual]
+theorem IsSuccLimit.ne_bot [OrderBot α] (h : IsSuccLimit a) : a ≠ ⊥ :=
+  h.bot_lt.ne'
 
 @[to_dual]
 theorem not_isSuccLimit_iff : ¬ IsSuccLimit a ↔ IsMin a ∨ ¬ IsSuccPrelimit a := by
@@ -268,10 +271,6 @@ theorem isSuccLimit_iff_of_orderBot [OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥
 @[deprecated (since := "2026-03-31")] alias isSuccLimit_iff := isSuccLimit_iff_of_orderBot
 @[deprecated (since := "2026-03-31")] alias isPredLimit_iff := isPredLimit_iff_of_orderTop
 
-@[to_dual lt_top]
-theorem IsSuccLimit.bot_lt [OrderBot α] (h : IsSuccLimit a) : ⊥ < a :=
-  h.ne_bot.bot_lt
-
 variable [SuccOrder α]
 
 @[to_dual]