Nuprl - Proof: pdivisor bound 1

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

1. a :

2. b :

3. a | b
4.

b | a

a<b

By:	FwdThru Thm* a:, b:. a \| b ab [3]

Generated subgoal:

1 5. ab
a<b
2 steps

About:

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