simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
  not_lt, Finset.range_one, Finset.mem_singleton]
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
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a < N ∧ (1 ≤ a → N ≤ a) ↔ a = 0