[STATEMENT]
lemma neg_int_pow_val:
  assumes "a \<in> nonzero Q\<^sub>p"
  shows "val (a[^]-(i::int)) = - (val (a[^]i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val (a [^] - i) = - val (a [^] i)
[PROOF STEP]
using int_pow_val[of a i]
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Q\<^sub>p \<Longrightarrow> val (a [^] i) = eint i * val a

goal (1 subgoal):
 1. val (a [^] - i) = - val (a [^] i)
[PROOF STEP]
by (metis Qp_int_pow_nonzero assms int_pow_ord mult_minus_left val_ord val_p_int_pow val_p_int_pow_neg)