# HG changeset patch
# User nipkow
# Date 1290791208 -3600
# Node ID a92d744bca5f840a834a23cf4b0f7f3427c1c1ea
# Parent  ed0add6f69a7b90f27e3b95cc8dce1201ea47dd0
new lemma

diff -r ed0add6f69a7 -r a92d744bca5f src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Nov 26 14:19:16 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 26 18:06:48 2010 +0100
@@ -2009,6 +2009,15 @@
     by (simp add: card_Diff_subset AB) 
 qed
 
+lemma diff_card_le_card_Diff:
+assumes "finite B" shows "card A - card B \<le> card(A - B)"
+proof-
+  have "card A - card B \<le> card A - card (A \<inter> B)"
+    using card_mono[OF assms Int_lower2, of A] by arith
+  also have "\<dots> = card(A-B)" using assms by(simp add: card_Diff_subset_Int)
+  finally show ?thesis .
+qed
+
 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
 apply (rule Suc_less_SucD)
 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)