proposition: Lemma sum_of_i2bis n: natp n -> csumb (Nintcc \1c n) id = (binom (csucc n) \2c).
proof: Proof. move => nN. rewrite - cardinal_pairs_le //. set (E:= Nintcc \1c n). set X:=Zo _ _ . set(f:= Lg E (fun k => Zo X (fun z => Q z = k))). have p1: X = unionb f. rewrite /f; set_extens x. move => xX; move/Zo_P: (xX) => [xs [le1 le2 le3]]; apply /setUb_P; aw. have qE:inc (Q x) E by have h:= (cleT le1 le2); apply /(Nint_ccP1 NS1 nN). by ex_tac; rewrite LgV//; apply: Zo_i. by move=> /setUb_P; aw; move => [y yE]; rewrite LgV//; move /Zo_P => []. have p2: f= disjointU_fam (Lg E (fun i => Nintcc card_one i)). rewrite /f /disjointU_fam; aw; apply: Lg_exten. move=> x xE; move: (xE)=> /(Nint_ccP1 NS1 nN) [ox xn]. have xN:= NS_le_nat xn nN. rewrite LgV//; set_extens t. move => /Zo_P [] /Zo_P [] /setX_P [pt _ qN] [oP pq _] qt. apply /indexed_P;split => //; apply /(Nint_ccP1 NS1 xN); split => //; ue. move /indexed_P => [pt] /(Nint_ccP1 NS1 xN) [pa pb] pc. apply: Zo_i => //; apply /Zo_P; rewrite pc. split => //; apply /setX_P; rewrite pc. split => //;apply:NS_le_nat pb xN. have ->: X = disjointU (Lg E (fun i => Nintcc \1c i)). by rewrite p1 p2 /disjointU. apply: Eqc_disjointU1. split;aww => i iE; rewrite ! LgV//. have iN:= (Nint_S iE). rewrite card_Nint1c // card_card; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)