∀ {α : Type u_1} {xs : List α} {p : α → Bool} {a : α},
  (∀ (n s : ℕ), List.findIdxNth.go p xs n s = List.findIdxNth p xs n + s) →
    ∀ (n : ℕ),
      List.findIdxNth p (a :: xs) (n + 1) =
        if n + 1 = 0 then if p a = true then 0 else List.findIdxNth p xs 0 + 1
        else if p a = true then List.findIdxNth p xs (n + 1 - 1) + 1 else List.findIdxNth p xs (n + 1) + 1