lean_workbook_plus_39163
OpenProve the Fibonacci identity
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39163 (n p : ℕ) : fib (n + p + 1) = fib (n + 1) * fib (p + 1) + fib n * fib p := by sorry
Source
Prove the Fibonacci identity
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39163 (n p : ℕ) : fib (n + p + 1) = fib (n + 1) * fib (p + 1) + fib n * fib p := by sorry