exact Nat.not_lt_zero _ h'
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l : List α
h : Sorted r l
i✝ j✝ : ℕ
x✝¹ : i✝ < j✝
h' : i✝ < 0
x✝ : j✝ < List.length []
⊢ False
no goals