proposition: Lemma Exercise5_3d n p: natp n -> natp p -> csumb (Nintc p) (Exercise5_3V n p) = \2c ^c p *c binom n p.
proof: Proof. move => nN pN. transitivity (csumb (Nintc p) (fun k => (binom n p) *c (binom p k) )). apply: csumb_exten => k /(NintcP pN) lmn. by rewrite [in RHS] cprodC; apply:Exercise5_3c. by rewrite - (sum_of_binomial pN) cprodC cprod2Dn (NintcE pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)