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 intro
  a,b:. (c:. c | a  c | b  c | 1)  CoPrime(a,b)
By: (RepUnfolds [`coprime`;`gcd_p`] 0)
THEN
(Backchain [`new_hyps`;Thm* a:. 1 | a])

Generated subgoals:

None

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

PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc