Nuprl - Proof: mul cancel in assoced 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul cancel in assoced 1

1. a :

2. b :

3. n :

4. n

a = n

a = -n

a = b

a = -b

By:

Analyze 4

Generated subgoals:

1 4. na = nb
a = b a = -b
1 step

2 4. na = -nb
a = b a = -b
1 step

About:

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

1	4. na = nb a = b a = -b	1 step
2	4. na = -nb a = b a = -b	1 step