(7steps 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 refl 1 1 1 1

1. x1 : 
2. x2 : 
  <x1,x2>.num<x1,x2>.den = <x1,x2>.num<x1,x2>.den


By: Fold `qnum` 0


Generated subgoal:

1   x1/x2.numx1/x2.den = x1/x2.numx1/x2.den
2 steps

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

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