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.refl
  | false =>
    apply Nat.le_of_succ_le
    exact findIdx_loop_ge x p stop h (i+1) hi
else
  rewrite [dif_neg hi]; assumption
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi : i ≤ stop
⊢ (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) ≥
    i
no goals