exact x.size.pred_le
case refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x
no goals