IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  k! == k!k

is mentioned by

Thm*  m,k:mk  k!m = ((k!)  ((k-m)!))[factorial_ratio2]
Thm*  m,k:mk  k! = (k-m)!k!m[factorial_ratio]

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

IteratedBinops Sections DiscrMathExt Doc