no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝³ : Group G
inst✝² : AddGroup A
inst✝¹ : Finite G
inst✝ : DecidableEq G
⊢ y ∈ zpowers x ↔ y ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (orderOf x))
rw [← mem_powers_iff_mem_zpowers, mem_powers_iff_mem_range_orderOf]