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