Nuprl - Proof: pos mul arg bounds 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pos mul arg bounds 1

1. a :

2. b :

3. a

b>0

a>0 & b>0

a<0 & b<0

By:	Inst: Thm* i,j:. i<j i = j i>j Using:[a \| 0] THEN CaseSplitNWay 3 Hyp:-1

Generated subgoals:

1 4. a<0
  a>0 & b>0  a<0 & b<0
3 steps

2 4. a = 0
  a>0 & b>0  a<0 & b<0
1 step

3 4. a>0
  a>0 & b>0  a<0 & b<0
3 steps

About:

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