diff -r 804dfa6d35b6 -r bdf8eb8f126b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Sep 06 11:31:01 2011 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Sep 06 14:25:16 2011 +0200
@@ -2054,6 +2054,11 @@
  apply(auto intro:ccontr)
 done
 
+lemma card_le_Suc_iff: "finite A \<Longrightarrow>
+  Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
+by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
+  dest: subset_singletonD split: nat.splits if_splits)
+
 lemma finite_fun_UNIVD2:
   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
   shows "finite (UNIV :: 'b set)"