Theorem: Turanpartition.bal_sum' (Turan4/Turanpartition.lean)

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ psum t P = (t + 1) * minP t P + card (largeParts h)
Tactic:
rw [bal_sum h, mul_add, mul_one, ← add_assoc, ← add_mul, parts_card_add h]
State after:
no goals