Nuprl - Proof: factors smaller2 1 1 1 1

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

1. k :

2. i : {2..k

}
3. j :

4. i

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

j = 1

By:	SimilarTo: i = k

Generated subgoal:

1 7. j = 1
i = k
1 step

About:

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