simp only [dif_neg hsize]
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : ¬x.start < x.stop
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : ¬x.start < x.stop
⊢ IsHeap lt x 0