Def  i  j  k == ij & jk

is mentioned by

Thm*  m,k:. 1  m  k  k!m = k(k-1)!(m-1)	[factorial_tail_via_iter_step_rw]
Thm*  m,k:. 1  m  k  (k',m':. k' = k-1  m' = m-1  k!m = kk'!m'  )	[factorial_tail_via_iter_step]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html