feat(combinatorics/stars_and_bars): Add a dedicated type for stars and bars

[eric-wieser]

---

[robertylewis]

@eric-wieser , is this file meant as a standalone "leaf node," or do you forsee uses for it in other developments? I'll admit, I've always thought of "stars and bars" as just a thing that can be counted with binomial coefficients, not as a data structure itself. So I'm wondering about the motivation for this new file.

[eric-wieser]

I've seen a bunch of cardinality arguments that just say "well this type is isomorphic to stars and bars in some obvious way, so the cardinality is the same". For such an argument to be visible in the lean code, we presumably need some stars_and_bars type.

I'll change this back to awaiting author though, since it probably does make sense to add the particular cardinality argument I had in mind, which is waiting on me to cleanup another PR.

[YaelDillies]

What's the status of this?