proposition: Lemma binom2a n: natp n -> \2c *c (binom (csucc n) \2c) = n *c (csucc n).
proof: Proof. move:n ; rewrite -{2} succ_one; apply: Nat_induction. rewrite cprod0l (binomSnSm NS0 NS1) (binom0Sm NS1) (binom1 NS0). by rewrite (Nsum0r NS0) cprod0r. move=> n nN r; move: (NS_succ nN) => sN. rewrite (binomSnSm sN NS1) cprodDr r (binom1 sN) - cprodDl cprodC. by rewrite - csum_11 (Nsucc_rw sN) (Nsucc_rw nN) csumA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)