simp [smallest, c]
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ smallest (head :: tail) hyp ∈ head :: tail
case neg
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
⊢ head ≤ smallest tail ⋯ ∨ Nat.min head (smallest tail ⋯) ∈ tail