num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* a:b:a | b  ab[divisor_bound]
cites the following:
Thm* a,b:n:ab  nanb[mul_preserves_le]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num thy 1 Sections StandardLIB Doc