(6steps total) PrintForm Definitions Lemmas rat 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq rat sym 1 1

1. x : 
2. y : 
3. x.numy.den=y.numx.den
  y.numx.den=x.numy.den


By: Analyze 2 THEN Analyze 1


Generated subgoal:

1 1. x1 : 
2. x2 : 
3. y1 : 
4. y2 : 
5. <x1,x2>.num<y1,y2>.den=<y1,y2>.num<x1,x2>.den
  <y1,y2>.num<x1,x2>.den=<x1,x2>.num<y1,y2>.den

3 steps

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

(6steps total) PrintForm Definitions Lemmas rat 1 Sections StandardLIB Doc