apply Nat.le_of_not_le
case h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ smallest tail ⋯ ≤ head
case h.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ ¬head ≤ smallest tail ⋯