Nuprl - Proof: factorial tail via iter zero 1 1

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

1. m :

2. k :

3. k<m

i:{(k-m)..k

}. i+1 = 0

By:	Witness: -1

Generated subgoals:

None

About:

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