no goals
α : Type ?u.37531
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
n : ℕ
⊢ a ^ bit0 n = (a * a) ^ n
rw [pow_bit0, (Commute.refl a).mul_pow]