[STATEMENT]
lemma idiv_by_0: "(a::enat) div 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 0 = 0
[PROOF STEP]
unfolding div_enat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a of enat x \<Rightarrow> case 0 of enat y \<Rightarrow> enat (x div y) | \<infinity> \<Rightarrow> 0 | \<infinity> \<Rightarrow> case 0 of enat 0 \<Rightarrow> 0 | enat (Suc n) \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>) = 0
[PROOF STEP]
by (case_tac a, simp_all)