have hkstop : k < stop :=
  trans (r:=LT.lt) (s:=LE.le) hk' <| findIdx_loop_le x p stop h i
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
⊢ p x[k] = false
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i k : Nat
hk : k ≥ i
hk' : k < findIdx.loop x p stop h i
x✝ : k < n
hkstop : k < stop
⊢ p x[k] = false