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

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (smallParts h) = t + 1 - card (largeParts h)
Tactic:
rw [← parts_card_add h,add_tsub_cancel_right]
State after:
no goals