proposition: Lemma fib_sum_square n: \sum_(i < n) (fib i)^2 = fib n * fib n.-1.
proof: Proof. elim:n=> [|n IH]; first by rewrite big_ord0. by rewrite big_ord_recr /= IH -mulnDr addnC mulnC; case: (n). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)