feat(Combinatorics): Combinatorial interpretations of the Stirling numbers

[thomaskwaring]

Prove that the Stirling numbers, defined in Mathlib by recursion, indeed count their associated combinatorial objects. While entirely elementary (on paper), this could be interesting as there is very little explicit (ie, counting the cardinality of some set or type) enumerative combinatorics in Mathlib.

[kim-em]

@thomaskwaring

I'm inclined to believe these are too easy. How many LoC would you estimate for solutions here? I'm guessing <2000 to do this nicely, possibly less?

[thomaskwaring]

that's fair, certainly <2000 maybe a lot less. it's a bit hard for me to judge the requirement "difficult for current frontier models" bc i haven't spent any time using them — i was comparing it to the Cayley graph problem but more than happy to defer to your judgement :)