proposition: Lemma nbos0: nb_odd_sums \0c = \1c.
proof: Proof. apply /set_of_card_oneP; apply/singletonP; split. have de: domain emptyset = emptyset by aw. exists emptyset; apply/odd_seqsP; split; last by rewrite csum_trivial. split; [apply: fgraph_set0 | rewrite de; apply: NS0 | ]. by hnf; rewrite de => t /in_set0. move => u v /odd_seqsP [qa qb] /odd_seqsP [qc qd]. move: (nbos_p1 qa) (nbos_p1 qc); rewrite qb qd => /cle0 du /cle0 dv. apply: fgraph_exten; [by case: qa | by case qc | by ue | ]. by rewrite du => t /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)