proposition: Lemma Fib_sums_odd n: natp n -> Fib (csucc (cdouble n)) = csucc (csumb (csucc n) (fun i => Fib (cdouble i))).
proof: Proof. move: n; apply: Nat_induction. rewrite cdouble0 succ_zero csumb1 cdouble0 Fib0 Fib1. by rewrite (card_card CS0) succ_zero. move => n nN Hrec. have snN:= NS_succ nN. have sN: natp (csumb (csucc n) (fun i : Set => Fib (cdouble i))). apply: finite_sum_finite; split. hnf; aw; move => t tn; bw => //; apply: NS_Fib; apply: NS_double. by move: (NS_inc_nat snN tn). by aw; apply: finite_set_nat. rewrite (csum_fs _ (NS_succ nN)) - (csum_Sn _ sN) - Hrec. by rewrite (double_succ nN) (Fib_rec (NS_succ (NS_double nN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)