feat(data/sym/card): Prove stars and bars (#11162)
In this file we prove (in `sym.card_sym_eq_multichoose`) that `multichoose (card α) k` counts the number of multisets of cardinality `k` over a finite alphabet `α`.
In conjunction with `nat.multichoose_eq`, which shows that `multichoose n k = choose (n + k - 1) k`, we immediately derive `card (sym α k) = (card α + k - 1).choose k`, which is the essence of the "stars and bars" technique in combinatorics.
Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>
Co-authored-by: Huỳnh Trần Khanh <qcdz9r6wpcbh59+github@gmail.com>
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
