(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
1. r : 
2. s : 
3. CoPrime(r,s)
4. x : 
5. y : 
6. rx+sy = 1
  x:. r | x-1 & s | x-0
By: Witness 1-rx

Generated subgoal:

1   r | 1-rx-1 & s | 1-rx-0
5 steps

About:
intnatural_numberaddsubtractmultiplyequalandexists
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