(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:
qmul
functionality
1
1
1.
p
:
2.
q
:
3.
r
:
4.
s
:
p
.num
q
.den =
q
.num
p
.den
r
.num
s
.den =
s
.num
r
.den
p
*q
r
.num
q
*q
s
.den =
q
*q
s
.num
p
*q
r
.den
By:
OnHyps [4;3;2;1] RatHD
Generated subgoal:
1
1.
p1
:
2.
p2
:
3.
q1
:
4.
q2
:
5.
r1
:
6.
r2
:
7.
s1
:
8.
s2
:
p1
/
p2
.num
q1
/
q2
.den =
q1
/
q2
.num
p1
/
p2
.den
r1
/
r2
.num
s1
/
s2
.den =
s1
/
s2
.num
r1
/
r2
.den
p1
/
p2
*q
r1
/
r2
.num
q1
/
q2
*q
s1
/
s2
.den =
q1
/
q2
*q
s1
/
s2
.num
p1
/
p2
*q
r1
/
r2
.den
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
rat
1
Sections
StandardLIB
Doc