no goals
β : Type ?u.15072
A : Type ?u.15075
G : Type ?u.15078
M : Type u_1
R : Type ?u.15084
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
n m : ℕ
ha : 1 ≤ a
h : n ≤ m
k : ℕ
hk : n + k = m
⊢ a ^ n * a ^ k = a ^ m
rw [← hk, pow_add]