--- a/src/HOL/Finite_Set.thy Mon May 03 19:06:33 2021 +0200
+++ b/src/HOL/Finite_Set.thy Mon May 03 21:49:30 2021 +0100
@@ -1811,6 +1811,10 @@
(\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
by (auto simp: card_insert_if card_gt_0_iff elim!: card_eq_SucD)
+lemma card_Suc_eq_finite:
+ "card A = Suc k \<longleftrightarrow> (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> finite B)"
+ unfolding card_Suc_eq using card_gt_0_iff by fastforce
+
lemma card_1_singletonE:
assumes "card A = 1"
obtains x where "A = {x}"