[STATEMENT]
lemma even_card':
  assumes "even(card A)" "x\<in>A"
  shows "\<exists>y\<in>A. y\<noteq>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>A. y \<noteq> x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>y\<in>A. y \<noteq> x)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y\<in>A. y \<noteq> x)

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>y\<in>A. y=x"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>A. y \<noteq> x)

goal (1 subgoal):
 1. \<forall>y\<in>A. y = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>A. y = x

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "A={x}"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>A. y = x

goal (1 subgoal):
 1. A = {x}
[PROOF STEP]
by (metis all_not_in_conv assms(2) insertI2 mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
A = {x}

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "card(A)=1"
[PROOF STATE]
proof (prove)
using this:
A = {x}

goal (1 subgoal):
 1. card A = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card A = 1

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
card A = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>even(card A)\<close>
[PROOF STATE]
proof (prove)
using this:
card A = 1
even (card A)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed