exact ⟨0, Nat.zero_lt_sub_of_lt hrng, rfl⟩
case succ.inr.refl
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
x : Subarray α
n : Nat
y : Array α
h : loop.OpSpec lt (popMax lt x) n y
hrng : x.start < x.stop
ge_start : x.start ≤ x.stop - 1
lt_stop : x.stop - 1 < x.stop
IH : ∀ (lt_stop : x.stop - 1 < (popMax lt x).stop), ∃ k hk, y[x.stop - 1] = (popMax lt x)[k]
⊢ ∃ k hk, x[0] = x[k]
no goals