# HG changeset patch
# User nipkow
# Date 1420893097 -3600
# Node ID a95b6f608a738aae2567b5b2fa7faa75a4ac84a5
# Parent  e743ce816cf6108178ab27ed098d2078cccc56ba
added lemma

diff -r e743ce816cf6 -r a95b6f608a73 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Jan 10 10:40:11 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Jan 10 13:31:37 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"