suffices ¬ Descendant n i from
  get_heapifyDown_not_descendant lt x n i this
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ (heapifyDown lt x n)[i] = x[i]
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : ¬Descendant n k
this : n < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ ¬Descendant n i