(5steps 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: gcd p zero rel
  a,b:. GCD(a;0;b)  a = b  a = -b
By: RepD THEN (Unfold `gcd_p` -1) THEN GenRepD

Generated subgoal:

1 1. a : 
2. b : 
3. b | a
4. b | 0
5. z:. z | a & z | 0  z | b
  a = b  a = -b
4 steps

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

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