. show ∀ k, x.size / 2 ≤ k → IsHeap lt x k
  intro k hk
  refine .leaf lt x k ?_
  rewrite [← Nat.div_add_mod x.size 2]
  refine Nat.add_le_add ?_ ?_
  . exact Nat.mul_le_mul_left 2 hk
  . apply Nat.le_of_succ_le_succ
    exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)