no goals
ι : Type ?u.112272
α : Type u_1
β : Type ?u.112278
f g : Perm α
p : α → Prop
x y z : α
n : ℤ
⊢ SameCycle f x (↑(f ^ n) y) ↔ SameCycle f x y
rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]