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
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
stop : Nat
h : stop ≤ n
i : Nat
hi✝ : i ≤ stop
hi : i < stop
⊢ (bif p x[i] then i else findIdx.loop x p stop h (i + 1)) ≥ i
no goals