exact IH h.left
case node_left
α : Type u
lt : α → α → Bool
x : Subarray α
i j✝ j : Nat
h✝ : Descendant (2 * j + 1) j✝
IH : IsHeap lt x (2 * j + 1) → IsHeap lt x j✝
h : IsHeap lt x j
⊢ IsHeap lt x j✝
no goals