∀ (x a : ℤ),
  (Int.fib x * Int.fib (a + 1) + Int.fib (x - 1) * Int.fib a) ^ 2 -
      Int.fib x *
        (Int.fib x * (Int.fib (a + 1) ^ 2 + Int.fib a ^ 2) +
          Int.fib (x - 1) * (Int.fib a * Int.fib (a + 1) + Int.fib (a - 1) * Int.fib a)) =
    (-1) ^ x.natAbs * Int.fib a ^ 2