(4steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: only one nat divs one 1 1

1. b : 
2. b | 1
3. c:. 1 = bc
  b = 1


By: Analyze-1


Generated subgoal:

1 3. c : 
4. 1 = bc
  b = 1

1 step

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

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