proposition: Lemma sum_of_binomial n: natp n -> csumb (csucc n) (binom n) = \2c ^c n.
proof: Proof. move=> nN. rewrite - card_setP. set (X:= Lg (csucc n) (fun p=>subsets_with_p_elements p n)). set (Y:= disjointU_fam X). have fgX: fgraph X by rewrite/ X; fprops. have fgY: fgraph Y by rewrite /Y/disjointU_fam; fprops. have dx: domain X = domain Y by rewrite /Y/disjointU_fam; aw. have eqv: forall i, inc i (domain X) -> (Vg X i) =c (Vg Y i). by move=> i idX; rewrite /Y/disjointU_fam LgV//; aw. have mdX: mutually_disjoint X. apply: mutually_disjoint_prop2. move=> i j y id jd;rewrite / subsets_with_p_elements. by move=> /Zo_hi yi /Zo_hi yj; rewrite -yi -yj. have mdY: mutually_disjoint Y by rewrite /Y; fprops. have <-:unionb X = \Po n. rewrite /X; set_extens t. by move /setUb_P; aw; move=> [y ydx]; rewrite LgV//; move /Zo_P => []. move => tp; apply /setUb_P; aw. have cxi: (inc (cardinal t) (csucc n)). apply /(NleP nN); move: (tp) => /setP_P /sub_smaller. by rewrite (card_nat nN). by ex_tac; rewrite LgV//; apply: Zo_i. rewrite (Eqc_disjointU (conj dx eqv) mdX mdY). apply: csum_pr3; fprops; rewrite /X;aw; trivial => i ix; rewrite !LgV//. move: (NS_inc_nat (NS_succ nN) ix) => iN. rewrite (card_p_subsets nN iN (card_nat nN)). exact: (card_nat (NS_binom nN iN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)