∀ {α : Type u_1} {x : α} [inst : BEq α] (head : α) (tail : List α) {n : ℕ},
  List.findIdxNth (fun x_1 => x_1 == x) (head :: tail) n + 1 ≤ (head :: tail).length →
    List.findIdxNth (fun x_1 => x_1 == x) (head :: tail) n < (head :: tail).length