(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definition of a commonly used ratio of factorials.
At:
factorial
ratio2
m
,
k
:
.
m
k
k
!
m
= ((
k
!)
((
k
-
m
)!))
By:
SimilarTo:
Thm*
m
,
k
:
.
m
k
k
! = (
k
-
m
)!
k
!
m
Generated subgoal:
1
1.
m
:
2.
k
:
3.
m
k
4.
k
! = (
k
-
m
)!
k
!
m
k
!
m
= ((
k
!)
((
k
-
m
)!))
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
m,k:
. m
k 
k!m = ((k!) 
((k-m)!)) m,k:. mk k!m = ((k!) ((k-m)!))m,k:. mk k! = (k-m)!
k!m
k
k!m
k!m = ((k!) ((k-m)!))
