Nuprl - Proof: fib coprime sfa2 1 1 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fib coprime sfa2 1 1 2 1 1 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
7.

x,y:

. fib(k-2)

x+fib(k-1)

y = 1

a,b:

. fib(k-2)

b+fib(k-1)

(a+b) = 1

By:	ExistHD Hyp:-1 THEN Witness: y-x \| x

Generated subgoals:

None

About:

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