feat(Order/SuccPred): succ a ≤ b ↔ a < b when b is not maximal

Author: SnirBroshi

Mathlib/Algebra/Order/SuccPred.lean

@@ -53,6 +53,9 @@ theorem add_one_le_of_lt (h : x < y) : x + 1 ≤ y := by
 theorem add_one_le_iff_of_not_isMax (hx : ¬ IsMax x) : x + 1 ≤ y ↔ x < y := by
   rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]
 
+theorem add_one_le_iff_of_not_isMax' (hy : ¬ IsMax y) : x + 1 ≤ y ↔ x < y := by
+  rw [← succ_eq_add_one, succ_le_iff_of_not_isMax' hy]
+
 @[simp]
 theorem add_one_le_iff [NoMaxOrder α] : x + 1 ≤ y ↔ x < y :=
   add_one_le_iff_of_not_isMax (not_isMax x)
@@ -231,6 +234,9 @@ theorem le_of_lt_add_one (h : x < y + 1) : x ≤ y := by
 theorem lt_add_one_iff_of_not_isMax (hy : ¬ IsMax y) : x < y + 1 ↔ x ≤ y := by
   rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]
 
+theorem lt_add_one_iff_of_not_isMax' (hx : ¬ IsMax x) : x < y + 1 ↔ x ≤ y := by
+  rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax' hx]
+
 @[simp]
 theorem lt_add_one_iff [NoMaxOrder α] : x < y + 1 ↔ x ≤ y :=
   lt_add_one_iff_of_not_isMax (not_isMax y)

Mathlib/Data/ENat/Basic.lean

@@ -299,8 +299,11 @@ lemma lt_one_iff_eq_zero : n < 1 ↔ n = 0 :=
 lemma le_one_iff_eq_zero_or_eq_one : n ≤ 1 ↔ n = 0 ∨ n = 1 :=
   Order.le_one_iff
 
-theorem lt_add_one_iff (hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
-  Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
+theorem lt_add_one_iff (hn : n ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
+  Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hn)
+
+theorem lt_add_one_iff' (hm : m ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
+  Order.lt_add_one_iff_of_not_isMax' (not_isMax_iff_ne_top.mpr hm)
 
 @[simp]
 theorem lt_two_iff : n < 2 ↔ n ≤ 1 := by
@@ -314,10 +317,6 @@ theorem add_le_add_iff_right {m n k : ENat} (h : k ≠ ⊤) :
     n + k ≤ m + k ↔ n ≤ m :=
   WithTop.add_le_add_iff_right h
 
-theorem lt_add_one_iff' {m n : ENat} (hm : m ≠ ⊤) :
-    m < n + 1 ↔ m ≤ n := by
-  rw [← add_one_le_iff hm, add_le_add_iff_right one_ne_top]
-
 theorem lt_coe_add_one_iff {m : ℕ∞} {n : ℕ} : m < n + 1 ↔ m ≤ n :=
   lt_add_one_iff (coe_ne_top n)
 

Mathlib/Order/SuccPred/Basic.lean

@@ -186,6 +186,12 @@ theorem lt_succ_of_le_of_not_isMax (hab : b ≤ a) (ha : ¬IsMax a) : b < succ a
 theorem succ_le_iff_of_not_isMax (ha : ¬IsMax a) : succ a ≤ b ↔ a < b :=
   ⟨(lt_succ_of_not_isMax ha).trans_le, succ_le_of_lt⟩
 
+@[to_dual le_pred_iff_of_not_isMin']
+theorem succ_le_iff_of_not_isMax' (hb : ¬IsMax b) : succ a ≤ b ↔ a < b := by
+  by_cases ha : IsMax a
+  · grind [le_succ, IsMax.mono]
+  · exact succ_le_iff_of_not_isMax ha
+
 @[to_dual]
 lemma succ_lt_succ_of_not_isMax (h : a < b) (hb : ¬ IsMax b) : succ a < succ b :=
   lt_succ_of_le_of_not_isMax (succ_le_of_lt h) hb
@@ -417,13 +423,19 @@ variable [LinearOrder α] [SuccOrder α] {a b : α}
 @[to_dual] lemma succ_min (a b : α) : succ (min a b) = min (succ a) (succ b) := succ_mono.map_min
 
 @[to_dual le_of_pred_lt]
-theorem le_of_lt_succ {a b : α} : a < succ b → a ≤ b := fun h ↦ by
-  by_contra! nh
-  exact (h.trans_le (succ_le_of_lt nh)).false
+theorem le_of_lt_succ {a b : α} : a < succ b → a ≤ b := by
+  contrapose!
+  exact succ_le_of_lt
 
 @[to_dual pred_lt_iff_of_not_isMin]
-theorem lt_succ_iff_of_not_isMax (ha : ¬IsMax a) : b < succ a ↔ b ≤ a :=
-  ⟨le_of_lt_succ, fun h => h.trans_lt <| lt_succ_of_not_isMax ha⟩
+theorem lt_succ_iff_of_not_isMax (ha : ¬IsMax a) : b < succ a ↔ b ≤ a := by
+  contrapose!
+  exact succ_le_iff_of_not_isMax ha
+
+@[to_dual pred_lt_iff_of_not_isMin']
+theorem lt_succ_iff_of_not_isMax' (hb : ¬IsMax b) : b < succ a ↔ b ≤ a := by
+  contrapose!
+  exact succ_le_iff_of_not_isMax' hb
 
 @[to_dual (reorder := ha hb)]
 theorem succ_lt_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) :