for n, r being non zero Element of NAT st r <= n holds
((Fib n) ^2) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2)