(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: gcd p shift 2
1. a : 
2. b : 
3. y : 
4. k : 
5. y | a
6. y | b
7. z:. z | a & z | b  z | y
8. z : 
9. z | a
10. z | b+ka
  z | y
By: InstHyp [z] 7

Generated subgoals:

1   z | b
5 steps
2 11. z | y
  z | y
Trivial

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