no goals
α : Type ?u.132793
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
rw [sub_eq_add_neg, zpow_add, zpow_neg]