rw [parts_card_add h,add_comm] at this
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : card (largeParts h) + succ 0 ≤ t + 1
⊢ card (largeParts h) ≤ t