(17steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Relevant to so-called permutation counting problems since these injections are the ways to order a distinct values chosen from a total of b values.

At: nsub inj factorial tail

  a,b:. (a inj b) ~ (b!a)
By: CompNatInd Concl

Generated subgoal:

1 1. a : 
2. a1:. a1<a  (b:. (a1 inj b) ~ (b!a1))
3. b : 
  (a inj b) ~ (b!a)
16 steps

About:
natural_numberall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(17steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Search Doc