apply Nat.le_of_not_lt
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ findIdx x p 0 n ≤ i
case a
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
i : Nat
hi : i < n
hp : p x[i] = true
⊢ ¬i < findIdx x p 0 n