Nuprl - Proof: fib coprime sfa2 1 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fib coprime sfa2 1 1 2 1

1. n :

n1:

. n1<n

(

. k = n1+1

(

x,y:

. fib(n1)

x+fib(k)

y = 1))
3. k :

4. k = n+1
5.

k = 0
6.

k = 1

a,b:

. fib(k-1)

a+(fib(k-1)+fib(k-2))

b = 1

By:	SimilarTo: a,b:. fib(k-2)b+fib(k-1)(a+b) = 1

Generated subgoal:

1 a,b:. fib(k-2)b+fib(k-1)(a+b) = 1
2 steps

About:

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