Nuprl - Proof: fib coprime 2 1 2 1

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

1. n :

2. 0<n
3. CoPrime(fib(-1+n),fib(n))
4.

1+n = 0 &

1+n = 1

CoPrime(fib(n),fib(-1+n)+fib(n))

By:	TryOnAllClauses (Unfold `coprime`) THEN SeqOnM [FwdThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y) [3] ;Using [`k',1] (FwdThru Thm* a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y) [-1]) ;ArithSimp -1]

Generated subgoals:

None

About:

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