ι : Type ?u.2442862
α : Type u_1
β : Type ?u.2442868
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ Nat.succ 0 ≤ card (support (cycleOf f x)) ↔ 2 ≤ card (support (cycleOf f x))
ι : Type ?u.2442862
α : Type u_1
β : Type ?u.2442868
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ 0 < card (support (cycleOf f x)) ↔ ↑f x ≠ x
rw [← two_le_card_support_cycleOf_iff, ← Nat.succ_le_iff]
no goals
ι : Type ?u.2442862
α : Type u_1
β : Type ?u.2442868
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
⊢ Nat.succ 0 ≤ card (support (cycleOf f x)) ↔ 2 ≤ card (support (cycleOf f x))
exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩