(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. a : 
2. p : 
3. prime(p)
4. CoPrime(p,a)
  p | a
By: (RWO Thm* a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1)) 4)
THEN
(Analyze 0)

Generated subgoal:

1 4. c:. c | p  c | a  (c ~ 1)
5. p | a
  False
4 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