proposition: Lemma Fib_sums_even n: natp n -> Fib (cdouble (csucc n)) = csumb (csucc n) (fun i => Fib(csucc (cdouble i))).
proof: Proof. move: n; apply: Nat_induction. rewrite succ_zero csumb1 cdouble0 succ_zero Fib1 (card_card CS1). by rewrite /cdouble (cprod1r CS2) Fib2. move => n nN Hrec. rewrite (csum_fs _ (NS_succ nN)) - Hrec. by rewrite - (Fib_rec (NS_double (NS_succ nN))) (double_succ (NS_succ nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)