[STATEMENT]
lemma (in padic_integers) p_res_ring_one:
  assumes "k > 0"
  shows "\<one>\<^bsub>Zp_res_ring k\<^esub> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>residue_ring (p ^ k)\<^esub> = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. \<one>\<^bsub>residue_ring (p ^ k)\<^esub> = 1
[PROOF STEP]
by (simp add: residue_ring_def)