exact IH (heapifyDown lt x n)
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), mkHeap.loop lt x n = Nat.foldRev (fun n x => heapifyDown lt x n) n x
x : Subarray α
⊢ mkHeap.loop lt x (Nat.succ n) = Nat.foldRev (fun n x => heapifyDown lt x n) (Nat.succ n) x
no goals