no goals
ι : Type ?u.204487
α : Type u_1
β : Type ?u.204493
f g : Perm α
p : α → Prop
x y z : α
n : ℕ
x✝ : SameCycle (f ^ n) x y
m : ℤ
h : ↑((f ^ n) ^ m) x = y
⊢ ↑(f ^ (↑n * m)) x = y
simp [zpow_mul, h]