feat(Data/Finset): card_eq_succ in terms of cons (#16951)

Also add `cons_ne_empty` and make it simp, also to match `insert_ne_empty`

Mathlib/Data/Finset/Basic.lean

@@ -778,6 +778,8 @@ theorem cons_nonempty (h : a ∉ s) : (cons a s h).Nonempty :=
 
 @[deprecated (since := "2024-09-19")] alias nonempty_cons := cons_nonempty
 
+@[simp] theorem cons_ne_empty (h : a ∉ s) : cons a s h ≠ ∅ := (cons_nonempty _).ne_empty
+
 @[simp]
 theorem nonempty_mk {m : Multiset α} {hm} : (⟨m, hm⟩ : Finset α).Nonempty ↔ m ≠ 0 := by
   induction m using Multiset.induction_on <;> simp

Mathlib/Data/Finset/Card.lean

@@ -683,6 +683,11 @@ lemma exists_of_one_lt_card_pi {ι : Type*} {α : ι → Type*} [∀ i, Decidabl
   obtain rfl | hne := eq_or_ne (a2 i) ai
   exacts [⟨a1, h1, hne⟩, ⟨a2, h2, hne⟩]
 
+theorem card_eq_succ_iff_cons :
+    s.card = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ t.card = n :=
+  ⟨cons_induction_on s (by simp) fun a s _ _ _ => ⟨a, s, by simp_all⟩,
+   fun ⟨a, t, _, hs, _⟩ => by simpa [← hs]⟩
+
 section DecidableEq
 variable [DecidableEq α]