[STATEMENT]
lemma nat_of_integer_non_positive [simp]:
  "k \<le> 0 \<Longrightarrow> nat_of_integer k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> 0 \<Longrightarrow> nat_of_integer k = 0
[PROOF STEP]
by transfer simp