have := con_sum h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ largeParts h = filter (fun i => ¬P i = minP t P) (range (t + 1))
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ largeParts h = filter (fun i => ¬P i = minP t P) (range (t + 1))