(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 1
1. b : 
2. 0<b
3. ((b-1) inj (b-1)) ~ ((b-1)!)
  (b(b-1)!) ~ (b!)
By: Use:[k:= b] Rewrite by Thm*  k:. k! = k(k-1)!  

Generated subgoals:

None

About:
intnatural_numbersubtractmultiplyless_thanequalall
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