(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card nat vs nat tuple 2 1 1
1. k : 
2. 1<k
3. ((k-1)) ~ 
  (((k-1))({(k-1)..k})) ~ ()
By: Rewrite by Hyp:3

Generated subgoal:

1   (({(k-1)..k})) ~ ()
1 step

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

(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc