\binom{n}{m} outside 0<=m<=n

[lars-hellstrom]

And another one for Chris:

The combinat1 CD states as only FMP of binomial the quotient-of-factorials formula, but as all discrete mathematicians know, it is very useful (and consistent) to have the binomial coefficients defined (to be 0) for m outside the 0 to n range where the factorial formula is valid.

As a minimal modification, I would suggest modifying the FMP to make 0<=m<=n a precondition for the factorial formula.

Adding the (Pascal's triangle) recursion as an FMP is probably also a good idea.

In that same CD, the Stirling numbers could also do with having their recursions stated as FMPs; these are a whole lot more natural than the closed formula that is provided. And the description of Stirling1 could state explicitly that these are the signed (or is alternating the more common term in English?) Stirling numbers of the first kind.