1.1 --- a/src/HOL/Finite_Set.thy	Fri Nov 26 17:54:15 2010 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 26 18:07:00 2010 +0100
     1.3 @@ -2009,6 +2009,15 @@
     1.4      by (simp add: card_Diff_subset AB) 
     1.5  qed
     1.6  
     1.7 +lemma diff_card_le_card_Diff:
     1.8 +assumes "finite B" shows "card A - card B \<le> card(A - B)"
     1.9 +proof-
    1.10 +  have "card A - card B \<le> card A - card (A \<inter> B)"
    1.11 +    using card_mono[OF assms Int_lower2, of A] by arith
    1.12 +  also have "\<dots> = card(A-B)" using assms by(simp add: card_Diff_subset_Int)
    1.13 +  finally show ?thesis .
    1.14 +qed
    1.15 +
    1.16  lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
    1.17  apply (rule Suc_less_SucD)
    1.18  apply (simp add: card_Suc_Diff1 del:card_Diff_insert)