let n be Element of NAT ; :: thesis: Fib n, Fib (n + 1) are_relative_prime
A1: n,n + 1 are_relative_prime by PEPIN:1;
(Fib n) gcd (Fib (n + 1)) = Fib (n gcd (n + 1)) by FIB_NUM:5
.= 1 by A1, INT_2:def 4, PRE_FF:1 ;
hence Fib n, Fib (n + 1) are_relative_prime by INT_2:def 4; :: thesis: verum