(7steps total) PrintForm Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: coprime prod 1 1

1. a : 
2. b1 : 
3. b2 : 
4. x,y:ax+b1y = 1
5. x,y:ax+b2y = 1
  x,y:ax+b1b2y = 1


By: OnHyps [5;6;4;5] Analyze THEN RenameVar `x2' 7 THEN RenameVar `y2' 8


Generated subgoal:

1 4. x1 : 
5. y1 : 
6. ax1+b1y1 = 1
7. x2 : 
8. y2 : 
9. ax2+b2y2 = 1
  x,y:ax+b1b2y = 1

4 steps

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

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