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