no goals
α : Type ?u.50460
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✝² : Monoid N
inst✝¹ : AddMonoid A
inst✝ : AddMonoid B
x : M
n : ℕ
hx : x ^ n = 1
hn : n ≠ 0
⊢ ↑(ofPowEqOne x n hx hn ^ n) = ↑1
simp [hx]