have := Nat.add_le_add (card_pos.mpr (small_nonempty h)) (le_refl (card (largeParts h)))
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (largeParts h) ≤ t
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t