# HG changeset patch
# User nipkow
# Date 1290791220 -3600
# Node ID 88f2955a111e0971250875b1fc13a0644a9ee718
# Parent  3ba17f07b23c241e6330c105ce026affd8a24e23# Parent  a92d744bca5f840a834a23cf4b0f7f3427c1c1ea
merged

diff -r 3ba17f07b23c -r 88f2955a111e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Nov 26 17:54:15 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 26 18:07:00 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)