Nuprl - Proof: self divisor mul 1

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

1. a :

2. b :

3. a

b | a

b ~ 1

By:	Assert ((ab) ~ (a1)) THENA ArithSimp 0

Generated subgoals:

1 (ab) ~ a
1 step

2 4. (ab) ~ (a1)
b ~ 1
1 step

About:

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