# HG changeset patch
# User wenzelm
# Date 1420904121 -3600
# Node ID fd9102b419f525a3bfc64ef93f303ddd6922f59b
# Parent  a95b6f608a738aae2567b5b2fa7faa75a4ac84a5# Parent  a74eb8e0907aa656a872e6658e31a9e76c64a7d1
merged

diff -r a74eb8e0907a -r fd9102b419f5 src/HOL/Finite_Set.thy
--- 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"