for n being Element of NAT holds Fib n, Fib (n + 1) are_coprime