n✝ n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
n✝ n : ℕ
⊢ Fintype.card (Composition n) = 2 ^ (n - 1)
rw [← compositionAsSet_card n]
no goals
n✝ n : ℕ
⊢ Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
exact Fintype.card_congr (compositionEquiv n)