(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factorial
ratio
1
1.
m
:
2.
k
:
3.
m
k
k
!
k
= (
k
-
m
)!(
k
-
m
)
k
!
m
By:
Inst:
Thm*
n
,
m
,
k
:
.
n
k
-
m
m
k
k
!(
n
+
m
) = (
k
-
m
)!
n
k
!
m
Using:[
k
-
m
|
m
|
k
]
Generated subgoal:
1
4.
k
!(
k
-
m
+
m
) = (
k
-
m
)!(
k
-
m
)
k
!
m
k
!
k
= (
k
-
m
)!(
k
-
m
)
k
!
m
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
k
k!k = (k-m)!(k-m)
k!m
k
k!k = (k-m)!(k-m)k!m
n,m,k:. nk-m 
mk k!(n+m) = (k-m)!nk!m Using:[k-m | m | k]k!m
k!k = (k-m)!(k-m)k!m
