Nuprl - Proof: factorial tail via iter zero

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

m,k:

. k<m

k!m = 0

By:	Def of k!m

Generated subgoal:

1 1. m :
2. k :
3. k<m
( i:{k-m..k}. i+1) = 0
2 steps

About:

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