no goals
ι : Type ?u.73203
α : Type u_1
β : Type ?u.73209
f g : Perm α
p : α → Prop
x y z : α
⊢ (∃ b, ↑(f ^ ↑(Equiv.addRight 1).symm b) (↑f x) = y) ↔ SameCycle f x y
simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]