Nuprl - Proof: nat prod one iff factors one 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat prod one iff factors one 2

x,y:

. x

y = 1

y = 1
2. x :

3. y :

4. x

y = 1

x = 1

By:	FwdThru: Hyp:1 on [ yx = 1 ]

Generated subgoals:

None

About:

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