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