if h : stop ≤ n then
  rewrite [dif_pos h]
  refine trans (r:=LE.le) ?_ h
  exact findIdx_loop_le x p stop h start
else
  rewrite [dif_neg h]
  exact findIdx_loop_le x p n .refl start
α : 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) ≤ n
no goals