exact ⟨Nat.pos_of_ne_zero (Ne.symm hzk), rfl⟩
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
k : Nat
hk✝ :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
hk : k < Subarray.size x - 1
hzk : ¬0 = k
⊢ 0 < k ∧ x[k] = x[k]
no goals