if hi : i < x.size then
  have hr : 2*i+2 ≥ x.size := .step hl
  refine .node' i hi ?_ ?_ (.out_of_range _ hl) (.out_of_range _ hr)
  . intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
  . intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
else
  exact .out_of_range i (Nat.ge_of_not_lt hi)
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
⊢ IsHeap lt x i
no goals