SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
a
,
b
:
. 0<
a
b
0<
a
& 0<
b
[pos_mul_arg_boundsNat]
cites the following:
3
Thm*
a
,
b
:
.
a
b
>0
a
>0 &
b
>0
a
<0 &
b
<0
[pos_mul_arg_bounds]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
SimpleMulFacts
Sections
DiscrMathExt
Doc
a,b:
. 0<a
b 
0<a & 0<ba,b:
. ab>0 a>0 & b>0 
a<0 & b<0a,b:. 0<ab 0<a & 0<ba,b:. ab>0 a>0 & b>0 a<0 & b<0