PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factorial
tail
via
iter
step
rw
m
,
k
:
. 1
m
k
k
!
m
=
k
(
k
-1)!(
m
-1)
By:
Auto
THEN
BackThru:
Thm*
m
,
k
:
. 1
m
k
(
k'
,
m'
:
.
k'
=
k
-1
m'
=
m
-1
k
!
m
=
k
k'
!
m'
)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
m,k:
. 1 
m k 
k!m = k
(k-1)!(m-1) m,k:. 1 m k k!m = k(k-1)!(m-1)m,k:. 1 m k (k',m':. k' = k-1 m' = m-1 k!m = kk'!m' 
)
