(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 2 1 1

1. a : 
2. p : 
3. prime(p)
4. p | a
5. c : 
6. c | p
7. c | a
8. p = 0
9. (p ~ 1)
10. a:a | p  (a ~ 1)  (a ~ p)
  c | 1


By: FwdThru 10 [6]


Generated subgoal:

1 11. (c ~ 1)  (c ~ p)
  c | 1

3 steps

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