∀ (n : ℤ) (m : ℕ),
  Int.fib (↑m - 1) * Int.fib n + Int.fib ↑m * Int.fib (n + 1) +
      (Int.fib (↑(m + 1) - 1) * Int.fib n + Int.fib ↑(m + 1) * Int.fib (n + 1)) =
    Int.fib (↑m - 1) * Int.fib n + Int.fib ↑m * Int.fib (n + 1) + Int.fib ↑m * Int.fib n +
      Int.fib (↑m + 1) * Int.fib (n + 1)