(12steps 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: coprime iff ndivides 1 1
1. a : 
2. p : 
3. prime(p)
4. c:. c | p  c | a  (c ~ 1)
5. p | a
  False
By: Unfold `prime` 3 THEN RepD

Generated subgoal:

1 3. p = 0
4. (p ~ 1)
5. b,c:. p | bc  p | b  p | c
6. c:. c | p  c | a  (c ~ 1)
7. p | a
  False
3 steps

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

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