Nuprl - Proof: factors smaller2 1 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

1. k :

2. i : {2..k

}
3. j :

4. i

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

i = k

By:	Rewrite4 by j = 1

Generated subgoals:

None

About:

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