Nuprl - Proof: only pm one divs one 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: only pm one divs one 1 1 1

1. b :

2. b | 1
3. b

1
4. b = 0

b = 1

By:	(HypSubst 4 2) THEN (FwdThru Thm* a:. 0 \| a a = 0 [2])

Generated subgoals:

None

About:

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