(7steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factors smaller2
  k:, i:{2..k}, j:. ij = k  2  j < k & i<k
By: UnivCD

Generated subgoal:

1 1. k : 
2. i : {2..k}
3. j : 
4. ij = k
  2  j < k & i<k
6 steps

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

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