--- a/src/HOL/Finite_Set.thy Mon Jul 20 11:40:43 2015 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jul 20 23:12:50 2015 +0100
@@ -1249,6 +1249,12 @@
apply(simp del:insert_Diff_single)
done
+lemma card_insert_le_m1: "n>0 \<Longrightarrow> card y \<le> n-1 \<Longrightarrow> card (insert x y) \<le> n"
+ apply (cases "finite y")
+ apply (cases "x \<in> y")
+ apply (auto simp: insert_absorb)
+ done
+
lemma card_Diff_singleton:
"finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
by (simp add: card_Suc_Diff1 [symmetric])