∀ {α : Type u_1} [inst : BEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)},
  ↑xc.snd + 1 ≤ (List.filter (fun x => x == xc.fst) xs).length →
    ↑xc.snd < (List.findIdxs (fun x => x == xc.fst) xs).length