The ratio of consecutive Fibonacci numbers

We prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio.

theorem tendsto_fib_succ_div_fib_atTop : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.fib (n + 1)) / ↑(Nat.fib n)) Filter.atTop (nhds Real.goldenRatio)

The limit of fib (n + 1) / fib n as n → ∞ is the golden ratio.

theorem tendsto_fib_div_fib_succ_atTop : Filter.Tendsto (fun (n : ℕ) => ↑(Nat.fib n) / ↑(Nat.fib (n + 1))) Filter.atTop (nhds (-Real.goldenConj))

The limit of fib n / fib (n + 1) as n → ∞ is the negative conjugate of the golden ratio.