if hstop : stop ≤ n then
  rewrite [dif_pos hstop] at hk'
  exact get_findIdx_loop_of_lt x p stop hstop start k hk hk'
else
  rewrite [dif_neg hstop] at hk'
  exact get_findIdx_loop_of_lt x p n .refl start k hk hk'
α : Type u
n : Nat
x : SizedArray α n
p : α → Bool
start stop k : Nat
hk : k ≥ start
hk' : k < if h : stop ≤ n then findIdx.loop x p stop h start else findIdx.loop x p n (_ : Nat.le n n) start
x✝ : k < n
⊢ p x[k] = false
no goals