cases Nat.lt_or_eq_of_le (Nat.le_pred_of_lt lt_stop) with
| inl hlt =>
  have ⟨k,hk,hy⟩ := IH (stop_popMax lt x hrng ▸ hlt)
  have ⟨l,hl,_,hx⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
  simp only [hy, hx]
  exact ⟨l, hl, rfl⟩
| inr heq =>
  cases heq
  rewrite [h.get_eq_of_ge_stop (x.stop-1) (stop_popMax lt x hrng ▸ .refl)]
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
case succ
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
i : Nat
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
ge_start : x.start ≤ i
lt_stop : i < x.stop
IH : ∀ (lt_stop : i < (popMax lt x).stop), ∃ k hk, y[i] = (popMax lt x)[k]
hrng : x.start < x.stop
⊢ ∃ k hk, y[i] = x[k]
no goals