Cassini and Catalan identities for the Fibonacci numbers

Cassini's identity states that for n : ℤ, fib (n + 1) * fib (n - 1) - fib n ^ 2 is equal to (-1) ^ |n|. And Catalan's identity states that for any integers x and a, we get fib (x + a) ^ 2 - fib x * fib (x + 2 * a) = (-1) ^ |x| * fib a ^ 2.

theorem Int.fib_succ_mul_fib_pred_sub_fib_sq (n : ℤ) : fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ n.natAbs

Cassini's identity: fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1) ^ |n|.

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

Catalan's identity: fib (x + a) ^ 2 - fib x * fib (x + 2 * a) = (-1) ^ |x| * fib a ^ 2.