proposition: Lemma fib_sum : forall n, \sum_(i < n) fib i = (fib n.+1).-1.
proof: Proof. elim=> [|n IH]; first by rewrite big_ord0. by rewrite big_ord_recr /= IH fibSS; case: fib (fib_gt0 _ (ltn0Sn n)). Qed.
imports: mathcomp(all_ssreflect all_algebra)