Nuprl - Proof: chrem exists 1 1 1

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

1. r :

2. s :

3. GCD(r;s;1)
4.

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

GCD(s;r;1)

By:	BackThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y)

Generated subgoals:

None

About:

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