no goals
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = x
⊢ ↑(f ^ (n + 1)) x = ↑f x
rw [pow_succ, mul_apply, h]
no goals
α : Type u_1
f g h✝ : Perm α
x : α
hffx : ↑f (↑f x) = x
n : ℕ
h : ↑(f ^ n) x = ↑f x
⊢ ↑(f ^ (n + 1)) x = x
rw [pow_succ, mul_apply, h, hffx]