proposition: Lemma fib_sum_square: forall n, \sum_(i < n) (fib i)^2 = fib n * fib n.-1.
proof: Proof. elim=> [|n IH]; first by rewrite big_ord0. rewrite big_ord_recr /= IH. by rewrite -mulnDr addnC; case: (n)=> // n1; rewrite -fibSS mulnC. Qed.
imports: mathcomp(all_ssreflect all_algebra)