proposition: Lemma binom2 n: natp n -> binom (csucc n) \2c = (n *c (csucc n)) %/c \2c.
proof: Proof. move=> nN; move: (NS_succ nN) => sN. apply: (cdivides_pr2 (NS_prod nN sN) NS2 (NS_binom sN NS2) card2_nz). by rewrite (binom2a nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)