α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ (n + 1 + 1)) x = x ∨ ↑(f ^ (n + 1 + 1)) x = ↑f x
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ Int.negSucc n) x = x ∨ ↑(f ^ Int.negSucc n) x = ↑f x
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ, eq_comm,
  inv_eq_iff_eq, ← mul_apply, ← pow_succ', @eq_comm _ x, or_comm]
no goals
α : Type u_1
f g h : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
⊢ ↑(f ^ (n + 1 + 1)) x = x ∨ ↑(f ^ (n + 1 + 1)) x = ↑f x
exact pow_apply_eq_of_apply_apply_eq_self hffx _