proposition: Lemma nbos_value n: natp n -> nb_odd_sums n = Yo (n = \0c) \1c (Fib n).
proof: Proof. have Ha F N: natp N -> csumb (csucc N) F = (csumb (csucc N -s1 \0c) F) +c (F \0c). move => nN; set p := (csucc N -s1 \0c). have ha: ~ (inc \0c p) by case /setC1_P. have <-: p +s1 \0c = csucc N by apply: setC1_K; apply/(NleP nN); apply: cle0n. by rewrite (csumA_setU1 _ ha). move => nN; move: (cleR (CS_nat nN)). move: n nN {- 2} n; apply: Nat_induction. by move => n /cle0 ->; Ytac0; rewrite nbos0. move => n nN Hrec p le1. have pN := NS_le_nat le1 (NS_succ nN). have hN:= NS_half pN. move: le1; case: (cdouble_halfV pN) => ->. move => le1. case: (equal_or_not (chalf p) \0c) => hz. by rewrite hz cdouble0 nbos0; Ytac0. move: (cpred_pr hN hz); set q := cpred _ ; move =>[sa sb]. rewrite sb { 2} (double_succ sa) (Y_false (@succ_nz _)). rewrite (Fib_sums_even sa) (nbos_rec_even sa) /csumb. apply: f_equal; apply: Lg_exten => i ilq. have iN:= (NS_inc_nat (NS_succ sa) ilq). have le2: csucc (cdouble i) <=c n. move: ilq; rewrite - sb => /(NltP hN) /(cleSltP iN). move/(double_monotone (NS_succ iN) hN) => h. move: (cleT h le1); rewrite double_succ //. by move/(cleSSP (CS_succ _) (CS_nat nN)). by rewrite (Hrec _ le2) (Y_false (@succ_nz _)). have c1: cardinalp (cdouble (chalf p)) by apply: CS_nat; apply: NS_double. have c2: cardinalp n by apply: CS_nat. move/(cleSSP c1 c2) => le1. rewrite (Fib_sums_odd hN) (nbos_rec_odd hN). rewrite (Y_false (@succ_nz _)). rewrite (Ha _ _ hN) (Ha _ _ hN) cdouble0 nbos0 Fib0. set s1 := csumb _ _; set s2 := csumb _ _. have Hb t: inc t (csucc (chalf p)) -> t <> \0c -> natp t /\ (nb_odd_sums (cdouble t)) = Fib (cdouble t). move => ta tb. have tN: natp t by apply: NS_inc_nat ta; apply: NS_succ. split => //. have le2: cdouble t <=c n. move /(NleP hN): ta => /(double_monotone tN hN) => h;exact: (cleT h le1). by rewrite (Hrec _ le2) (Y_false (proj1 (double_nz tN tb))). have ns1: natp s1. apply: finite_sum_finite; split. hnf; aw; move => t ts; bw => //; case/setC1_P: ts => [ta tb]. by move: (Hb _ ta tb) => [tc ->]; apply: (NS_Fib (NS_double tc)). aw; apply: sub_finite_set (finite_set_nat (NS_succ hN)); apply: sub_setC. have cs2: cardinalp s2 by rewrite /s2 /csumb; fprops. rewrite - (Nsucc_rw ns1) (csum0r cs2). rewrite /csumb; congr csucc; congr csum; apply: Lg_exten. move => t/setC_P [ta /set1_P tb]; exact: (proj2 (Hb _ ta tb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)