proposition: Lemma sum_of_gen_binom2 n: natp n -> csumb (csucc n) (binom n) = \2c ^c n.
proof: Proof. move=> nN; symmetry. have cnn:=(card_nat nN). rewrite -(cardinal_set2 C0_ne_C1) -/C2 - (sum_of_gen_binom C2 nN cnn). set f:= fun m => (variantLc m (n -c m)). rewrite(@csum_Cn2 _ _ (csucc n) f). apply: csumb_exten => x xi;aw. by rewrite (card_partitions_p4 nN (NS_inc_nat (NS_succ nN) xi) cnn). split => //. + move=> m /(NleP nN) mn; move: (cdiff_pr mn) => e1. rewrite /f;apply /(graphs_sum_eqP _ nN);split => //;aww. hnf; aw => i itp; try_lvariant itp; [ exact:proj31 mn | fprops ]. + rewrite /f;move=> u v ui vi s; move: (f_equal (Vg ^~C0) s); aw; trivial. + move=> y / (graphs_sum_eqP _ nN) [dy sy fgy alc]. rewrite /cardinal_fam /allf dy in alc. move: (alc _ inc_C0_C2) (alc _ inc_C1_C2) => ca cb. have abn: (Vg y C0) +c (Vg y C1) = n. by rewrite - csum2_pr0 - sy - csum_gr dy. move: (nN); rewrite -abn => nN'. move: (NS_in_suml ca nN')(NS_in_sumr cb nN') => aN bN. move: (csum_M0le (Vg y C1) ca); rewrite abn => an. exists (Vg y C0); first by apply /NleP. rewrite /f;apply: fgraph_exten; aww. rewrite dy;move=> x xtp; try_lvariant xtp; trivial. rewrite -abn csumC cdiff_pr1 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)