(8steps total) Remark PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: chrem exists aux 1
1. r : 
2. s : 
3. CoPrime(r,s)
  x:. r | x-1 & s | x-0
By: (FwdThru Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1) [3])
THEN
(ExistHD -1)

Generated subgoal:

1 4. x : 
5. y : 
6. rx+sy = 1
  x:. r | x-1 & s | x-0
6 steps

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

(8steps total) Remark PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc