feat: a few lemmas on WithTop ℕ∞ (#17164)

To be used when `WithTop ℕ∞` becomes the set of smoothness exponents, in #17152

Mathlib/Data/ENat/Basic.lean

@@ -259,4 +259,26 @@ theorem nat_induction {P : ℕ∞ → Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀
   · exact htop A
   · exact A _
 
+lemma add_one_nat_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : m < n) : (m + 1 : ℕ) ≤ n := by
+  match n with
+  | ⊤ => exact le_top
+  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
+  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using h
+
+@[simp] lemma coe_top_add_one : ((⊤ : ℕ∞) : WithTop ℕ∞) + 1 = (⊤ : ℕ∞) := rfl
+
+@[simp] lemma add_one_eq_coe_top_iff (n : WithTop ℕ∞) :
+    n + 1 = (⊤ : ℕ∞) ↔ n = (⊤ : ℕ∞) := by
+  match n with
+  | ⊤ => exact Iff.rfl
+  | (⊤ : ℕ∞) => exact Iff.rfl
+  | (n : ℕ) => norm_cast; simp only [coe_ne_top, iff_false, ne_eq]
+
+@[simp] lemma nat_ne_coe_top (n : ℕ) : (n : WithTop ℕ∞) ≠ (⊤ : ℕ∞) := ne_of_beq_false rfl
+
+lemma one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} :
+    1 ≤ n ↔ n ≠ 0 :=
+  ⟨fun h ↦ (zero_lt_one.trans_le h).ne',
+    fun h ↦ add_one_nat_le_withTop_of_lt (pos_iff_ne_zero.mpr h)⟩
+
 end ENat