Update BinomialNotes

Additional plans

BinomialNotes

@@ -27,24 +27,27 @@ Theorems about series we need:
 Part III, Implementation plan:
 
 Introduce ascending factorials Ring.ascFactorial r k, for r in a semiring R following data.nat.factorial.basic.
-This is a shift by one of Pochhammer.eval that makes some definitions cumbersome.
+Ring.ascFactorial is a shift by one of Pochhammer.eval that makes some definitions cumbersome.
 ascFactorial r k lies in the subsemiring of R generated by r, so in principle, proofs can be done in a commutative semiring.
 
 Define binomial semirings by injective Pnat multiplication and the divisibility criterion.
 Show that N is a binomial semiring.
 Define Ring.multichoose r k.
-Prove multichoose_mul using ascFactorial_mul.
+Prove multichoose_mul using ascFactorial_mul.  Also, "pascal's triangle" relation.
+Prove a multichoose vanderMonde for commuting x and y.
 
 Then, introduce descending factorials Ring.descFactorial r k, for r in a ring R.
 Compare with ascFactorial, compare descFactorial r k with descFactorial (k-r-1) k, prove descFactorial_mul.
 
 Introduce binomial coefficients Ring.choose r k.  compare with Nat.choose and Ring.multichoose.
+Compare Ring.choose r k with Ring.choose (k-r-1) k, prove Ring.choose_mul.
+vanderMonde.
 
 Part IV, To do:
 
 1. Figure out how to reduce proofs in the noncommutative case to the commutative semiring.
 
-2. Figure out how to take k! | x(x+1)⋯(x+k-1) and produce an element (exists.intro?)
+2. Figure out how to take k! | x(x+1)⋯(x+k-1) and produce an element (exists.intro?).
 
-3. Later, consider proving some of Elliott's other results, like how the integer-valued polynomial rings (generated by x.choose n) are universal binomial rings. 
+3. Later, consider proving some of Elliott's other results, like how the integer-valued polynomial rings (generated by Ring.choose x n) are universal (commutative) binomial rings.