(7steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat prod one iff factors one
  x,y:. xy = 1  x = 1 & y = 1
By: x,y:. xy = 1  y = 1  Asserted

Generated subgoals:

1 1. x : 
2. y : 
3. xy = 1
  y = 1
3 steps
2 1. x,y:. xy = 1  y = 1
2. x : 
3. y : 
4. xy = 1
  x = 1
1 step
3 1. x,y:. xy = 1  y = 1
2. x : 
3. y : 
4. xy = 1
  y = 1
1 step
4 1. x,y:. xy = 1  y = 1
2. x : 
3. y : 
4. x = 1
5. y = 1
  xy = 1
1 step

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

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