Theorem: Turanpartition.parts_card_add (Turan4/Turanpartition.lean)

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (smallParts h) + card (largeParts h) = t + 1
Tactic:
rw [← card_range (t + 1), parts_union h, card_disjoint_union (parts_disjoint h)]
State after:
no goals