[STATEMENT]
lemma aadd_0_r: "x + (0::ant) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + 0 = x
[PROOF STEP]
apply (cut_tac mem_ant[of "x"], simp add:Zero_ant_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity> \<Longrightarrow> x + ant 0 = x
[PROOF STEP]
apply ((erule disjE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z. x = ant z) \<or> x = \<infinity> \<Longrightarrow> x + ant 0 = x
[PROOF STEP]
apply (erule disjE, erule exE, simp add:a_zpz,
       simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done