Nuprl - Proof: divisor bound 1 1 2

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

1. a :

2. b :

3. c :

4. b = a

c
5. c

By:	Using [`n',a] (FwdThru Thm* a,b:, n:. ab nanb [5])

Generated subgoal:

1 6. a1ac
ab
Auto

About:

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