exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) }) ≠ i
no goals