Nuprl - Proof: chrem exists aux 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: chrem exists aux 1 1 1

1. r :

2. s :

3. CoPrime(r,s)
4. x :

5. y :

6. r

x+s

y = 1

r | 1-r

x-1 & s | 1-r

x-0

By:

Analyze 0

Generated subgoals:

1 r | 1-rx-1
2 steps

2 s | 1-rx-0
2 steps

About:

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