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

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

1. n :

2. 0<n
3.

. k = n-1+1

(

x,y:

. fib(n-1)

x+fib(k)

y = 1)
4. k :

5. k = n+1
6.

k = 0
7.

k = 1
8.

x,y:

. fib(n-1)

x+fib(n)

y = 1

a,b:

. fib(n-1)

b+fib(n)

(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