PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial via intseg step
  k,n:. k = n+1  k! = kn!  
By: Def of <nat>!
THEN
BackThru: 
Thm*  m,k:. 1  m  k  (k',m':. k' = k-1  m' = m-1  k!m = kk'!m'  )

Generated subgoals:

None

About:
intnatural_numberaddsubtractmultiplyequalimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc