Nuprl - Proof: factorial tail via iter step

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial tail via iter step

m,k:

. 1

(

k',m':

. k' = k-1

m' = m-1

k!m = k

k'!m')

By:	Def of k!m

Generated subgoal:

1 1. m :
2. k :
3. 1m
4. mk
5. k' :
6. m' :
7. k' = k-1
8. m' = m-1
( i:{k-m..k}. i+1) = kk'!m'
4 steps

About:

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