no goals
α : Type ?u.26055
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✝¹ : Monoid M
inst✝ : AddMonoid A
a : M
m n : ℕ
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n
rw [← pow_add, Nat.sub_add_cancel h]