(3steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: coprime elim
  a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1))
By: (RepUnfolds [`coprime`;`gcd_p`;`assoced`] 0) THEN GenRepD
THEN
(Try (BackThru Thm* a:. 1 | a))

Generated subgoals:

1 1. a : 
2. b : 
3. 1 | a
4. 1 | b
5. z:. z | a & z | b  z | 1
6. c : 
7. c | a
8. c | b
  c | 1
1 step
2 1. a : 
2. b : 
3. c:. c | a  c | b  c | 1 & 1 | c
4. z : 
5. z | a
6. z | b
  z | 1
1 step

About:
intnatural_numberimpliesall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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