induction n generalizing x with
| zero => rfl
| succ n IH => exact IH (heapifyDown lt x n)
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ mkHeap.loop lt x n = Nat.foldRev (fun n x => heapifyDown lt x n) n x
no goals