[STATEMENT]
lemma nat_of_natural_numeral [simp]:
  "nat_of_natural (numeral k) = numeral k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_of_natural (numeral k) = numeral k
[PROOF STEP]
by transfer rule