fib_two_mul_add_two — Mathlib

English

For all n, fib(2n+2) = fib(n+1) (2 fib(n) + fib(n+1)).

Русский

Для всех n выполняется fib(2n+2) = fib(n+1) (2 fib(n) + fib(n+1)).

LaTeX

$$fib(2n+2) = fib(n+1) (2 fib(n) + fib(n+1))$$

Lean4

theorem fib_two_mul_add_two (n : ℕ) : fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1)) :=
  by
  rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
  have : fib n ≤ 2 * fib (n + 1) := le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
  zify [this]
  ring

Похожие утверждения