α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
⊢ IsThreeCycle f⁻¹⁻¹⁻¹ → IsThreeCycle f⁻¹⁻¹
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
⊢ IsThreeCycle f⁻¹ → IsThreeCycle f
rw [← inv_inv f]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ f : Perm α
⊢ IsThreeCycle f⁻¹⁻¹⁻¹ → IsThreeCycle f⁻¹⁻¹
apply inv