Theorem: coe_fib_eq (LeanCourse/Lectures/Lecture7Before.lean)

State before:
n✝ n : ℕ
⊢ ↑(fib n) = (ϕ ^ n - ψ ^ n) / (ϕ - ψ)
Tactic:
sorry
State after:
no goals