Nuprl - Proof: factor smaller 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factor smaller 1

1. i : {2...}
2. j : {1...}

j<i

By:	Inst: Thm* a,b:, n:. a<b na<nb Using:[1 \| i \| j]

Generated subgoal:

1 3. j1<ji
j<ij
Auto

About:

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