2. 0<k
3.
p:{p:(
(k-1)
)| 
i:(k-1). p(i) }.
3. (least i:
. p(i)) 
{i:(k-1)| p(i) & (j:i. 
p(j)) }
4. p :
k
5. i :
k
6. p(i)
7.
p(0)
8. (least i:
. p(i+1)) (k-1)
9. p((least i:
. p(i+1))+1)
10.
j:(least i:. p(i+1)). p(j+1)
11. (least i:
. p(i+1))
12. j :
((least i:. p(i+1))+1)
13. j = 0
p(j)
