∀ {α : Type u_1} {xs : List α} {p : α → Bool} {a : α},
  (∀ (n s : ℕ), List.findIdxNth.go p xs n s = List.findIdxNth p xs n + s) →
    List.findIdxNth p (a :: xs) 0 =
      if 0 = 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 (0 - 1) + 1 else List.findIdxNth p xs 0 + 1