Nuprl - Proof: pdivisor bound 2

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

1. a :

2. b :

3. a<b
4. a | b

b | a

By:	(Analyze 0) THEN (Assert (a ~ b) THENA Analyze 0)

Generated subgoal:

1 5. b | a
6. a ~ b
False
1 step

About:

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