Nuprl - Proof: chrem exists aux a 1 1 1 1 1 2

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

1. r :

2. s :

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

5. y :

6. r

x+s

y = 1

s | s

By:	Backchain [Thm* a,b:. a \| b a \| -b;Thm* a,b,c:. a \| b a \| bc;Thm* a:. a \| a]

Generated subgoals:

None

About:

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