proposition: Lemma binom_2plus0 n: natp n -> binom (csucc n) \2c = (binom n \2c) +c n.
proof: Proof. move=> nN. by rewrite - succ_one (binomSnSm nN NS1) (binom1 nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)