if hi : i < stop then
  rewrite [dif_pos hi]; dsimp
  match p (x[i]'(trans (r:=LT.lt) (s:=LE.le) hi h)) with
  | true => exact Nat.le_of_lt hi
  | false => exact findIdx_loop_le x p stop h (i+1)
else
  rewrite [dif_neg hi]
  exact .refl
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
⊢ (if hi : i < stop then
      let_fun this := (_ : i < n);
      bif p x[i] then i else findIdx.loop x p stop h (i + 1)
    else stop) ≤
    stop
no goals