no goals
ι : Type ?u.31228
α : Type u_1
β : Type ?u.31234
f g : Perm α
p : α → Prop
x y z : α
x✝¹ : SameCycle f x y
x✝ : SameCycle f y z
i : ℤ
hi : ↑(f ^ i) x = y
j : ℤ
hj : ↑(f ^ j) y = z
⊢ ↑(f ^ (j + i)) x = z
rw [zpow_add, mul_apply, hi, hj]