simp only [mkHeap.loop, IH, size_as_heapifyDown]
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), Array.size (mkHeap.loop lt x n).as = Array.size x.as
x : Subarray α
⊢ Array.size (mkHeap.loop lt x (Nat.succ n)).as = Array.size x.as
no goals