ext a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a ∈ Finset.Ico 0 N \ Finset.Ico 1 N ↔ a ∈ Finset.range 1