no goals
α : Type ?u.103818
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 R
a : R
m n : ℕ
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]