[STATEMENT]
lemma int_pow_def2: "a [^]\<^bsub>G\<^esub> z =
   (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> (nat (-z))) else a [^]\<^bsub>G\<^esub> (nat z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^]\<^bsub>G\<^esub> z = (if z < 0 then inv\<^bsub>G\<^esub> (a [^]\<^bsub>G\<^esub> nat (- z)) else a [^]\<^bsub>G\<^esub> nat z)
[PROOF STEP]
by (simp add: int_pow_def nat_pow_def)