proposition: Lemma sum_of_i n: natp n -> csumb n id = binom n \2c.
proof: Proof. move: n; apply: Nat_induction. by rewrite (binom_bad NS0 NS2 clt_02) csum_trivial0. move=> n nN hr;rewrite induction_on_sum // hr binom_2plus0 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)