(8steps total) 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 a 1
1. r : 
2. s : {s':| CoPrime(r,s') }
  x:. ((x = 1 mod r) & (x = 0 mod s))
By: Analyze 2 THEN UnhideSqStableHyp 3

Generated subgoal:

1 2. s : 
3. CoPrime(r,s)
  x:. ((x = 1 mod r) & (x = 0 mod s))
6 steps

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

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