refine trans (r:=LE.le) ?_ h
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ n
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop : Nat
h : stop ≤ n
⊢ findIdx.loop x p stop h start ≤ stop