Nuprl - Proof: pdivisor bound

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

, b:

. a | b &

b | a

a<b & a | b

By:

GenRepD

Generated subgoals:

1 1. a :
2. b :
3. a | b
4. b | a
a<b
3 steps

2 1. a :
2. b :
3. a<b
4. a | b
b | a
2 steps

About:

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

1	1. a : 2. b : 3. a \| b 4. b \| a a<b	3 steps
2	1. a : 2. b : 3. a<b 4. a \| b b \| a	2 steps