Nuprl - Proof: factors smaller2 1 1 1

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

1. k :

2. i : {2..k

}
3. j :

4. i

j = k
5. i>0
6. j>0

By:	j = 1 Asserted

Generated subgoal:

1 j = 1
2 steps

About:

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