proposition: Lemma Exercise5_3e n p: natp n -> natp p -> p <> \0c -> csumb (Nintc_even p) (Exercise5_3V n p) = csumb (Nintc_odd p) (Exercise5_3V n p).
proof: Proof. move => nN pN pnz. set A:= (Nintc_even p); set B:= (Nintc_odd p). transitivity (csumb A (fun k => (binom n p) *c (binom p k) )). apply: csumb_exten => k /Zo_S /(NintcP pN) lmn. by rewrite [in RHS] cprodC; apply:Exercise5_3c. transitivity (csumb B (fun k => (binom n p) *c (binom p k))); last first. apply: csumb_exten => k /Zo_S /(NintcP pN) lmn; symmetry. by rewrite [in RHS] cprodC; apply:Exercise5_3c. by rewrite - cprod2Dn - cprod2Dn Exercise5_2_alt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)