(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Relevant to permutation counting problems since these injections are the finite permutations.

At: nsub inj factorial2

  b:. (b inj b) ~ (b!)
By: NatInd Concl

Generated subgoals:

1   (0 inj 0) ~ (0!)
5 steps
2 1. b : 
2. 0<b
3. ((b-1) inj (b-1)) ~ ((b-1)!)
  (b inj b) ~ (b!)
4 steps

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

(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc