case h
M : Type u_1
A : Type ?u.128599
B : Type ?u.128602
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}
M : Type u_1
A : Type ?u.128599
B : Type ?u.128602
inst✝ : Monoid M
n : M
⊢ powers n = closure {n}
ext
no goals
case h
M : Type u_1
A : Type ?u.128599
B : Type ?u.128602
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}
exact mem_closure_singleton.symm