∀ {α : Type u_1} (l : List α) (L : List (List α)) (i : ℕ),
  ¬List.findIdx (fun x => decide (l.length + x > i)) (List.map List.length L).partialSums = 0 →
    0 < List.findIdx (fun x => decide (i < l.length + x)) (List.map List.length L).partialSums