no goals
ι : Type ?u.78068
α : Type u_1
β : Type ?u.78074
f g : Perm α
p : α → Prop
x y z : α
n : ℤ
⊢ (∃ b, ↑(f ^ ↑(Equiv.addRight n).symm b) (↑(f ^ n) x) = y) ↔ SameCycle f x y
simp [SameCycle, zpow_add]