induction h with
| zero => rfl
| @succ x n y h IH =>
  specialize @IH hi <| Nat.le_trans (stop_popMax_le_stop lt x) hge
  exact Eq.trans IH <| get_as_popMax_of_ge_stop lt x i hge
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt x n y
i : Nat
hi : i < Array.size y
hge : i ≥ x.stop
⊢ y[i] = x.as[i]
no goals