have : n ≤ 2 * n := by
  rewrite [Nat.two_mul]; exact Nat.le_add_left n n
α : 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
⊢ IsHeap lt (heapifyDown lt x n) n
α : 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 ≤ 2 * n
⊢ IsHeap lt (heapifyDown lt x n) n