Nuprl - Proof: nsub mul 2 2 1

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

1. a :

2. 0<a
3.

b,c:

. (a-1)

b = c

((

(a-1)

b) ~

c)
4. b :

5. c :

6. a

b = c
7. 1

((

(a-1)

b)+

b) ~

By:	Use:[c:= c-b] Rewrite by Hyp:3

Generated subgoal:

1 ((c-b)+b) ~ c
1 step

About:

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