Nuprl - Proof: fib coprime sfa3 1 2 1 1

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

1. n :

. k<n

(

x,y:

. fib(k)

x+fib(k+1)

y = 1)
3.

n+1 = 1
4.

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 subgoal:

1 4. x :
5. y :
6. fib(n-1)x+fib(n)y = 1
fib(n-1)x+fib(n)(y-x+x) = 1
Auto

About:

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