proposition: Lemma sum_fib_pascal n: \sum_(i<n.+1) 'C(n,i)* fib i = fib(n.*2) /\ \sum_(i<n.+1) 'C(n,i)* fib i.+1 = fib(n.*2.+1).
proof: Proof. elim:n; first by rewrite !big_ord_recr !big_ord0 /= //. move =>n [He Ho]; split. rewrite big_ord_recl muln0 add0n doubleS fibSS - Ho. have ->: fib n.*2 = \sum_(i < n.+1) 'C(n, i.+1) * fib i.+1. by rewrite -He big_ord_recl big_ord_recr muln0 add0n bin_small //= addn0. by rewrite addnC -big_split; apply:eq_bigr=> i _ /=; rewrite - mulnDl/= binS. rewrite doubleS fibSS fibSS -Ho - He big_ord_recl bin0 muln1 /=. transitivity (\sum_(i < n.+1) 'C(n, i) * fib (bump 0 i).+1 + \sum_(i < n.+2) 'C(n, i) * fib i.+1). rewrite (big_ord_recl (n.+1)) bin0 muln1 [RHS] addnC - addnA; congr addn. by rewrite -big_split; apply:eq_bigr=> i _ /=; rewrite - mulnDl/= binS. rewrite (big_ord_recr (n.+1)) bin_small //= addn0;congr addn. by rewrite -big_split; apply:eq_bigr=> i _ /=; rewrite - mulnDr/= fibSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)