[STATEMENT]
lemma icard_insert_disjoint: "x \<notin> A \<Longrightarrow> icard (insert x A) = eSuc (icard A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<notin> A; finite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
 2. \<lbrakk>x \<notin> A; infinite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (simp add: icard_finite eSuc_enat card_insert_disjoint)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; infinite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (simp add: infinite_insert)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done