proposition: Lemma nbos_rec_even n: natp n -> nb_odd_sums (cdouble (csucc n)) = csumb (csucc n) (fun i => nb_odd_sums(csucc (cdouble i))).
proof: Proof. move => nN. have dN: natp (cdouble (csucc n)) by apply: NS_double; apply:NS_succ. have dnz: cdouble (csucc n) <> \0c. by rewrite double_succ //; apply succ_nz. rewrite (nbos_rec dN dnz) (odd_half (NS_succ nN)) (fct_sum_rev _ nN). rewrite /csumb; congr csum; apply: Lg_exten => i id. have iN: natp i by apply: (NS_inc_nat (NS_succ nN) id). have sdnN: natp (csucc (cdouble n)) by apply: NS_succ; apply: NS_double. have dnN: natp (cdouble n) by apply: NS_double. have le1: n -c i <=c n by apply: (cdiff_le1 _ (CS_nat nN)). have le2: cdouble (n -c i) <=c cdouble n. by apply/(double_monotone (NS_diff i nN) nN). have diN: natp (cdouble (n -c i)) by apply:NS_double; apply: NS_diff. rewrite (double_succ nN) (cdiff_pr6 sdnN diN) (cdiffSn (NS_double nN) le2). apply: f_equal; 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)