[Merged by Bors] - feat (RingTheory/Binomial) : Multichoose at negative arguments

[ScottCarnahan]

This PR adds some lemmas for evaluating Pochhammer polynomials and the multichoose function at negative arguments. This is preparation for identities involving generalized binomial coefficients.

---

[github-actions]

PR summary 1e6d7c9d85

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ multichoose_neg_add
+ multichoose_neg_of_lt
+ multichoose_neg_self
+ multichoose_neg_succ
+ multichoose_succ_neg_natCast
+ smeval_ascPochhammer_int_ofNat
+ smeval_ascPochhammer_nat_cast
+ smeval_ascPochhammer_neg_add
+ smeval_ascPochhammer_neg_of_lt
+ smeval_ascPochhammer_self_neg
+ smeval_ascPochhammer_succ_neg
+ smeval_neg_nat

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[Ruben-VandeVelde]

Some minor comments

[kim-em]

If you can make Ruben and my final suggested changes, this looks good. Apologies this took so long!

bors d+

[mathlib-bors]

✌️ ScottCarnahan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ScottCarnahan]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style