proposition: Lemma sum_of_i2 n: natp n -> csumb (Nintcc \1c n) id = (binom (csucc n) \2c).
proof: Proof. move => nN. rewrite -(sum_of_i3 (NS_succ nN)) -(NintE (NS_succ nN)) - (Nint_co_cc nN). move: (sum_of_i3 (NS_succ nN)). move: (Nint_pr5 nN) => [<- pb]. rewrite csumA_setU1 // csum0r // /csumb ; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)