α : Type u_1
β : Type ?u.815557
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ 1 < length l ↔ 2 ≤ length l
α : Type u_1
β : Type ?u.815557
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x ≠ x ↔ 2 ≤ length l
rw [Ne.def, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
no goals
α : Type u_1
β : Type ?u.815557
inst✝ : DecidableEq α
l : List α
x✝ : α
hl : Nodup l
x : α
hx : x ∈ l
⊢ 1 < length l ↔ 2 ≤ length l
exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩