no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
σ τ : { x // x ∈ alternatingGroup α }
hσ : IsThreeCycle ↑σ
hτ : IsThreeCycle ↑τ
⊢ Finset.card (support ↑σ) + 2 ≤ card α
rwa [hσ.card_support]