# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1620074970 -3600
# Node ID 58aed6f71f903b72c5f97b77cad73fc2ff857143
# Parent  0c8d6bec6491291ab4eba0e45fff19da13bfc2b4
A nice cardinality lemma

diff -r 0c8d6bec6491 -r 58aed6f71f90 src/HOL/Finite_Set.thy
--- 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}"