[STATEMENT]
lemma enat_coexhaust:
  obtains (0) "n = 0"
     | (eSuc) n' where "n = eSuc n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "n \<in> enat_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> enat_set
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> enat_set

goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> enat_set

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by cases (erule that)+
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed