exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
case node_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i✝ j : Nat
hj : j < Subarray.size x
i : Nat
hd : Descendant (2 * i + 1) j
IH : IsHeap lt x (2 * i + 1) → lt x[2 * i + 1] x[j] = false
h : IsHeap lt x i
⊢ lt x[i] x[j] = false
no goals