constructor <;>
rintro ⟨i, hi⟩
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
⊢ y ∈ zpowers x ↔ ∃ n < orderOf x, x ^ n = y
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
⊢ ∃ n < orderOf x, x ^ n = y

case mpr.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℕ
hi : i < orderOf x ∧ x ^ i = y
⊢ y ∈ zpowers x