[STATEMENT]
lemma Qp_int_pow_add: 
  fixes n::int 
  fixes m::int
  assumes "a \<in> nonzero Q\<^sub>p"
  shows "a [^] (n + m) = (a [^] n) \<otimes> (a [^] m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] (n + m) = a [^] n \<otimes> a [^] m
[PROOF STEP]
using monoid.int_pow_add[of Q\<^sub>p a n m] Units_eq_nonzero assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Group.monoid Q\<^sub>p; a \<in> Units Q\<^sub>p\<rbrakk> \<Longrightarrow> a [^] (n + m) = a [^] n \<otimes> a [^] m
Units Q\<^sub>p = nonzero Q\<^sub>p
a \<in> nonzero Q\<^sub>p

goal (1 subgoal):
 1. a [^] (n + m) = a [^] n \<otimes> a [^] m
[PROOF STEP]
by (simp add: Qp.monoid_axioms)