proposition: Lemma nbos1: nb_odd_sums \1c = \1c.
proof: Proof. apply /set_of_card_oneP; apply/singletonP; split. set f := (Lg C1 (fun z => \1c)). have df: domain f = singleton C0 by rewrite /f; aw. have vf: Vg f C0 = \1c by rewrite /f LgV//; apply: set1_1. have sf: csum f = \1c by rewrite (csum_trivial1 df) vf (card_card CS1). exists f; apply/odd_seqsP; split => //; rewrite /f. split; [ fprops | aw; apply:NS1| hnf; aw => t /set1_P ->]. rewrite vf; apply: odd_one. move => u v /odd_seqsP [qa qb] /odd_seqsP [qc qd]. move: (nbos_p1 qa) (nbos_p1 qc); rewrite qb qd. case: (equal_or_not (domain u) \0c) => duz. by move: qb; rewrite csum_trivial// => h; case:C0_ne_C1. case: (equal_or_not (domain v) \0c) => dvz. by move: qd; rewrite csum_trivial// => h; case:C0_ne_C1. case/cle_eqVlt; [move => du1 | by move/clt1]. case/cle_eqVlt; [move => dv1 | by move/clt1]. move: qa qc => [ra rb rc] [rd re rf]. have ha: inc \0c (domain u) by rewrite du1; apply: set1_1. have hb: inc \0c (domain v) by rewrite dv1; apply: set1_1. have duc: cardinalp (Vg u \0c) by apply: CS_nat; case: (rc C0 ha). have dvc: cardinalp (Vg v \0c) by apply: CS_nat; case: (rf C0 hb). move: qb qd. rewrite (csum_trivial1 du1) (csum_trivial1 dv1). rewrite ! card_card // => su sv. apply: fgraph_exten; fprops; try ue. rewrite du1 => y /set1_P ->; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)