Nuprl - Proof: chrem exists 1 1

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

1. r :

2. s :

3. CoPrime(r,s)
4.

. (x = 1 mod r) & (x = 0 mod s)

CoPrime(s,r)

By:	OnClauses [3;0] UnfoldTopAb

Generated subgoal:

1 3. GCD(r;s;1)
4.
5.
6. x:. (x = 1 mod r) & (x = 0 mod s)
GCD(s;r;1)
1 step

About:

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