diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index c15812a0ffbe9f..8d54a9ce9776f2 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -64,4 +64,8 @@ protected theorem le_add_self [AddCommMagma α] [LE α] [CanonicallyOrderedAdd 
   · rw [← WithBot.coe_add, WithBot.coe_le_coe]
     exact le_add_self
 
+lemma lt_zero_iff_eq_bot {α : Type*} [AddMonoid α] [Preorder α] [CanonicallyOrderedAdd α]
+    (a : WithBot α) : a < 0 ↔ a = ⊥ := by
+  induction a <;> simp
+
 end WithBot
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
index 78e40424a46ed9..423e99d10d634e 100644
--- a/Mathlib/Data/ENat/Basic.lean
+++ b/Mathlib/Data/ENat/Basic.lean
@@ -279,6 +279,11 @@ theorem succ_def (m : ℕ∞) : Order.succ m = m + 1 :=
 theorem add_one_le_iff (hm : m ≠ ⊤) : m + 1 ≤ n ↔ m < n :=
   Order.add_one_le_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)
 
+theorem add_one_le_iff' (hn : n ≠ ⊤) : m + 1 ≤ n ↔ m < n := by
+  rcases eq_or_ne m ⊤ with rfl | hm
+  · simpa
+  · exact add_one_le_iff hm
+
 theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=
   Order.one_le_iff_pos.trans pos_iff_ne_zero
 
@@ -607,6 +612,9 @@ end ENat
 
 namespace ENat.WithBot
 
+@[simp]
+lemma coe_eq_natCast (n : ℕ) : (n : ℕ∞) = (n : WithBot ℕ∞) := rfl
+
 lemma lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m := by
   rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
   cases n
@@ -621,6 +629,17 @@ lemma add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m := b
   · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
       ← WithBot.coe_lt_coe, WithBot.coe_natCast]
 
+lemma add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} : n + 1 ≤ m ↔ n < m := by
+  induction n with
+  | bot => simp
+  | coe n =>
+    norm_cast
+    simp [add_one_le_iff']
+
+@[simp]
+lemma add_one_le_zero_iff (n : WithBot ℕ∞) : n + 1 ≤ 0 ↔ n = ⊥ :=
+  add_one_le_natCast_iff.trans (WithBot.lt_zero_iff_eq_bot n)
+
 @[simp]
 lemma add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} : a + c = b + c ↔ a = b :=
   (IsAddRightRegular.all c).withTop.withBot.eq_iff