feat: four small lemmas about successors of finite cardinals (#11544)

Co-authored-by: @fpvandoorn 

<!-- The text above the `

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -1488,6 +1488,17 @@ theorem nat_succ (n : ℕ) : (n.succ : Cardinal) = succ ↑n := by
   rw [← Nat.cast_succ]
   exact natCast_lt.2 (Nat.lt_succ_self _)
 
+lemma succ_natCast (n : ℕ) : Order.succ (n : Cardinal) = n + 1 := by
+  rw [← Cardinal.nat_succ]
+  norm_cast
+
+lemma natCast_add_one_le_iff {n : ℕ} {c : Cardinal} : n + 1 ≤ c ↔ n < c := by
+  rw [← Order.succ_le_iff, Cardinal.succ_natCast]
+
+lemma two_le_iff_one_lt {c : Cardinal} : 2 ≤ c ↔ 1 < c := by
+  convert natCast_add_one_le_iff
+  norm_cast
+
 @[simp]
 theorem succ_zero : succ (0 : Cardinal) = 1 := by norm_cast
 #align cardinal.succ_zero Cardinal.succ_zero
@@ -1551,6 +1562,10 @@ theorem lt_aleph0 {c : Cardinal} : c < ℵ₀ ↔ ∃ n : ℕ, c = n :=
     exact ⟨Infinite.natEmbedding S⟩, fun ⟨n, e⟩ => e.symm ▸ nat_lt_aleph0 _⟩
 #align cardinal.lt_aleph_0 Cardinal.lt_aleph0
 
+lemma succ_eq_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : Order.succ c = c + 1 := by
+  obtain ⟨n, hn⟩ := Cardinal.lt_aleph0.mp h
+  rw [hn, succ_natCast]
+
 theorem aleph0_le {c : Cardinal} : ℵ₀ ≤ c ↔ ∀ n : ℕ, ↑n ≤ c :=
   ⟨fun h n => (nat_lt_aleph0 _).le.trans h, fun h =>
     le_of_not_lt fun hn => by