--- a/src/HOL/Finite_Set.thy Sat Jan 10 16:35:07 2015 +0100
+++ b/src/HOL/Finite_Set.thy Sat Jan 10 16:35:21 2015 +0100
@@ -1322,6 +1322,14 @@
shows "card (A \<union> B) = card A + card B"
using assms card_Un_Int [of A B] by simp
+lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
+apply(cases "finite A")
+ apply(cases "finite B")
+ using le_iff_add card_Un_Int apply blast
+ apply simp
+apply simp
+done
+
lemma card_Diff_subset:
assumes "finite B" and "B \<subseteq> A"
shows "card (A - B) = card A - card B"