n:
. CoPrime(fib(n),fib(n+1))a:
. GCD(a;1;1)a,b,y,k:. GCD(a;b;y) 
GCD(a;b+k
a;y)a,b,y:. GCD(a;b;y) GCD(b;a;y)| Rank | Theorem | Name |
| 2 | n:. CoPrime(fib(n),fib(n+1)) | [fib_coprime] |
| cites the following: | ||
| 1 | a:. GCD(a;1;1) | [gcd_p_one] |
| 1 | a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) | [gcd_p_shift] |
| 0 | a,b,y:. GCD(a;b;y) GCD(b;a;y) | [gcd_p_sym] |