proposition: Lemma nbos_rec_odd n: natp n -> nb_odd_sums (csucc (cdouble n)) = csumb (csucc n) (fun i => nb_odd_sums (cdouble i)).
proof: Proof. move => nN. have dN: natp (csucc (cdouble n)) by apply: NS_succ; apply:NS_double. have dnz: csucc (cdouble n) <> \0c by apply succ_nz. rewrite (nbos_rec dN dnz) - (double_succ nN) (even_half (NS_succ nN)). rewrite (fct_sum_rev _ nN) /csumb; congr csum; apply: Lg_exten => i id. have iN: natp i by apply: (NS_inc_nat (NS_succ nN) id). have ddN: natp (cdouble (n -c i)) by apply: NS_double; apply: NS_diff. rewrite (cdiff_pr6 (NS_double nN) ddN) ; apply: f_equal. move/(NleP nN): id => lin. by rewrite - {1} (cdiff_pr lin) -(double_sum) cdiff_pr1 //; apply: NS_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)