# HG changeset patch
# User nipkow
# Date 1752782782 -3600
# Node ID 5d2a599f88af56a2b5e72e6d563c2d69716d8bb8
# Parent  d26ffa4a1817c3830f391eac32d8ff5fea3658bb
moved lemma

diff -r d26ffa4a1817 -r 5d2a599f88af src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jul 17 20:09:42 2025 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Jul 17 21:06:22 2025 +0100
@@ -2239,6 +2239,11 @@
   then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
 qed
 
+corollary finite_arbitrarily_large_disj:
+  "\<lbrakk> \<not> finite(UNIV::'a set); finite (A::'a set) \<rbrakk> \<Longrightarrow> \<exists>B. finite B \<and> card B = n \<and> A \<inter> B = {}"
+using infinite_arbitrarily_large[of "UNIV - A"]
+by fastforce
+
 text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets
 and to show that their cardinalities are uniformly bounded. This possibility is formalized in
 the next criterion.\<close>
@@ -2969,11 +2974,6 @@
   with \<open>infinite S\<close> show False by simp
 qed
 
-corollary finite_arbitrarily_large_disj:
-  "\<lbrakk> infinite(UNIV::'a set); finite (A::'a set) \<rbrakk> \<Longrightarrow> \<exists>B. finite B \<and> card B = n \<and> A \<inter> B = {}"
-using infinite_arbitrarily_large[of "UNIV - A"]
-by fastforce
-
 proposition infinite_coinduct [consumes 1, case_names infinite]:
   assumes "X A"
     and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"