no goals
α : Type u_1
β : Type ?u.277786
γ : Type ?u.277789
δ : Type ?u.277792
inst✝ : CommMonoid α
a : α
n : ℕ
⊢ Associates.mk (a ^ n) = Associates.mk a ^ n
induction n <;> simp [*, pow_succ, Associates.mk_mul_mk.symm]