Nuprl - Proof: pdivisor bound 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pdivisor bound 1 1 1

1. a :

2. b :

3. a | b
4.

b | a
5. a

b
6. a = b

a<b

By:	(HypSubst 6 4) THEN (Analyze 4) THEN RelRST

Generated subgoals:

None

About:

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