Nuprl - Proof: nsub mul 2

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

1. a :

2. 0<a
3.

b,c:

. (a-1)

b = c

((

(a-1)

b) ~

c)
4. b :

5. c :

6. a

b = c

(

b) ~

By:	OOCinterpolate (((a-1)b)+b)

Generated subgoals:

1 (ab) ~ (((a-1)b)+b)
1 step

2 (((a-1)b)+b) ~ c
3 steps

About:

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