apply totally_ordered_of_sorted h₂
case neg
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ r (a₂ :: as)[k] (a₂ :: as)[l]
case neg.a
α : Type
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Trans r r r
inst✝ : Transitive r
l✝ : List α
h✝ : Sorted r l✝
i j : ℕ
a₁ a₂ : α
as : List α
h₁ : r a₁ a₂
h₂ : Sorted r (a₂ :: as)
hi✝ : i < List.length (a₁ :: a₂ :: as)
hj✝ : j < List.length (a₁ :: a₂ :: as)
l : ℕ
hj : l + 1 < List.length (a₁ :: a₂ :: as)
hl : l + 1 = j
this✝ : l < List.length (a₂ :: as)
hl' : (a₁ :: a₂ :: as)[l + 1] = (a₂ :: as)[l]
h : ¬i = 0
k : ℕ
h' : Nat.succ k < l + 1
hi : Nat.succ k < List.length (a₁ :: a₂ :: as)
hk : i = Nat.succ k
this : k < List.length (a₂ :: as)
hk' : (a₁ :: a₂ :: as)[k + 1] = (a₂ :: as)[k]
⊢ k < l