n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
rw [two_mul, fib_add]
no goals
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
ring