dsimp [findIdx]
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ findIdx x p start stop ≤ stop
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
⊢ (if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start) ≤ stop