(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
m
,
k
:
.
m
k
k
! = (
k
-
m
)!
k
!
m
By:
Def of <nat>!
Generated subgoal:
1
1.
m
:
2.
k
:
3.
m
k
k
!
k
= (
k
-
m
)!(
k
-
m
)
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! = (k-m)!
k!m m,k:. mk k! = (k-m)!k!m
k
k!k = (k-m)!(k-m)k!m
