(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
  r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))
By: Unfold `eqmod` 0 THEN UnivCD

Generated subgoal:

1 1. r : 
2. s : 
3. CoPrime(r,s)
  x:. r | x-1 & s | x-0
7 steps

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