cases heq
case succ.inr
α : 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
heq : i = x.stop - 1
⊢ ∃ k hk, y[i] = x[k]
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, y[x.stop - 1] = x[k]