Nuprl - Proof: factorial tail via iter step rw

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial tail via iter step rw

m,k:

. 1

k!m = k

(k-1)!(m-1)

By:	Auto THEN BackThru: Thm* m,k:. 1 m k (k',m':. k' = k-1 m' = m-1 k!m = kk'!m' )

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html