DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
10
Thm*
(
k
inj
k
) ~
(
k
!)
[nsub_inj_factorial]
cites the following:
9
Thm*
(
a
inj
b
) ~
(
b
!
a
)
[nsub_inj_factorial_tail]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
k inj
k) ~ (k!)a inj b) ~ (b!a)k inj k) ~ (k!)a inj b) ~ (b!a)