induction hd with
| refl => exact LawfulLTBRel.irrefl _
| node_left i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
| node_right i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_right _) (IH h.right)
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
h : IsHeap lt x i
j : Nat
hj : j < Subarray.size x
hd : Descendant i j
⊢ lt x[i] x[j] = false
no goals