exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
x✝ : k < n
hstop : stop ≤ n
hk' : k < findIdx.loop x p stop hstop start
⊢ p x[k] = false
no goals