rwa [← zpow_ofNat, Int.natAbs_of_nonneg hnonneg]
case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y
no goals