(10steps total) Remark Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj factorial2 2 1
1. b : 
2. 0<b
3. ((b-1) inj (b-1)) ~ ((b-1)!)
  (b((b-1) inj (b-1))) ~ (b!)
By: Rewrite by Hyp:3

Generated subgoal:

1   (b((b-1)!)) ~ (b!)
2 steps

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

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