DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
5
Thm*
k
:
.
k
! =
k
(
k
-1)!
[factorial_via_intseg_step_rw]
cites the following:
4
Thm*
k
,
n
:
.
k
=
n
+1
k
! =
k
n
!
[factorial_via_intseg_step]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
k:
. k! = k
(k-1)! 
k,n:. k = n+1 
k! = kn! k:. k! = k(k-1)! k,n:. k = n+1 k! = kn!