sum of the first n fibonacci numbers is the n+2'th fibonacci number - 1

fib.lean

import tactic
open nat

@[simp] def fib : ℕ -> ℕ
| 0 := 0
| 1 := 1
| (succ (succ n)) := fib n + fib (succ n)

@[simp] def sum_first_fib : ℕ -> ℕ
| 0 := 0
| (succ n) := fib (succ n) + sum_first_fib n

lemma one_le_fib_succ (n : ℕ) : 1 ≤ fib n.succ :=
begin
  induction n with n Ihn,
  simp,
  unfold fib,
  rw add_comm,
  apply le_add_of_le_of_nonneg,
  -- 1 ≤ fib n.succ
  exact Ihn,
  -- 0 ≤ fib n
  simp,
end

theorem sum_first_fib_closed_form (n : ℕ) :
  sum_first_fib n = fib (succ (succ n)) - 1 :=
begin
  induction n with n Ihn,
  { simp },
  { simp,
    rw Ihn,
    simp,
    -- fib n.succ + (fib n + fib n.succ - 1) =
    -- fib n.succ + (fib n + fib n.succ) - 1
    rw <- nat.add_sub_assoc,
    -- 1 ≤ fib n + fib n.succ
    rw add_comm,
    -- 1 ≤ fib n.succ + fib n
    apply le_add_of_le_of_nonneg,
    apply one_le_fib_succ,
    simp,
  }
end