Theorem: Pos.pow_assoc (Extra/Pos/Lemmas.lean)

State before:
x : Pos
y z : Nat
⊢ (x ^ y) ^ z = x ^ (y * z)
Tactic:
rw [Pos.pow_mul]
State after:
no goals