lean_workbook_plus_14129
OpenProve the statement for nonnegative .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14129 : ∀ k : ℕ, fib k + fib (k + 1) = fib (k + 2) := by sorry
Source
Prove the statement for nonnegative .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14129 : ∀ k : ℕ, fib k + fib (k + 1) = fib (k + 2) := by sorry