IteratedBinops
Sections
DiscrMathExt
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
5
Thm*
m
,
k
:
.
m
k
k
! = (
k
-
m
)!
k
!
m
[factorial_ratio]
cites the following:
4
Thm*
n
,
m
,
k
:
.
n
k
-
m
m
k
k
!(
n
+
m
) = (
k
-
m
)!
n
k
!
m
[factorial_tail_split_mid]
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops
Sections
DiscrMathExt
Search
Doc
m,k:
. m
k 
k! = (k-m)!
k!mn,m,k:. nk-m mk k!(n+m) = (k-m)!nk!mm,k:. mk k! = (k-m)!k!mn,m,k:. nk-m mk k!(n+m) = (k-m)!nk!m