n:. CoPrime(fib(n),fib(n+1))

By:	Rewrite by Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1) THEN CompNatInd Concl

1

1. n :  2. k:. k<n  (x,y:. fib(k)x+fib(k+1)y = 1)   a,b:. fib(n)a+fib(n+1)b = 1

6 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html