induction n generalizing x with
| zero => rfl
| succ n IH => dsimp [mkHeap.loop]; rw [IH, stop_heapifyDown]
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ (mkHeap.loop lt x n).stop = x.stop
no goals